{"entities":{"Q1663225":{"pageid":1673966,"ns":120,"title":"Item:Q1663225","lastrevid":68084856,"modified":"2026-04-12T21:20:16Z","type":"item","id":"Q1663225","labels":{"en":{"language":"en","value":"Toward compositional verification of interruptible OS kernels and device drivers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6921415"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$2BC97017-1186-480F-8358-D3E1408D63C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"93980419f2884557e152f885a01a62c8748bcf28","datavalue":{"value":{"text":"Toward compositional verification of interruptible OS kernels and device drivers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1663225$1F86C442-8D11-4212-B7A5-71D952DF043F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d4a6447cd0ce81d349fbe92841d4175bcd525595","datavalue":{"value":"1451.68170","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$A4C959E7-0AB2-46C1-A7D0-A9A1BA985F11","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e21d3e92f985fb5bc6926dc5ef8ef1b4f71f06c9","datavalue":{"value":{"entity-type":"item","numeric-id":328692,"id":"Q328692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$6720AC4C-D864-454B-85E4-AD51DC916610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0b5d47e6de599c5948ba694244e5d3d4341fa37","datavalue":{"value":{"entity-type":"item","numeric-id":1663222,"id":"Q1663222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$7468674E-126E-4ADB-BDCB-43B6DB9FB249","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b45204622bfa7b343b3d270acbf7de72b0faad61","datavalue":{"value":{"entity-type":"item","numeric-id":835763,"id":"Q835763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$60FF34CB-C9B6-42E3-BD64-73C1379C75F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e1b3813f9011abcf9ac098a6973796e9bb7caa6e","datavalue":{"value":{"entity-type":"item","numeric-id":1663223,"id":"Q1663223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$1B8BD971-E4EB-4611-8D48-CCEAEBFA2DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4a18eff36f23247ba49762bc37c9e8e013a5ca82","datavalue":{"value":{"entity-type":"item","numeric-id":1663224,"id":"Q1663224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$37AF82F5-784C-40CC-AF6A-DC6ADF808887","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$6B5E02A4-1902-454F-AEF1-B67C9107112E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1dea8b353f71cbbb3b5cacc724847e34eb1031d7","datavalue":{"value":{"time":"+2018-08-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1663225$5EEBFB65-A5A6-4305-BDB4-47A996F09292","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$4B5FA04A-304A-488F-9922-C437AD1C694E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$F9AD2458-926A-4B37-AA23-81DE47F4AEDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$58D2EFAC-81FD-48CB-B10F-CEF7006CCCC0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"afde04031b118714821cbc3ebec86580fb50a6fa","datavalue":{"value":"6921415","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$1A8C3339-DBF0-430F-8F0B-79FDB8BA55BB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$A1BB81D8-C4D5-4981-A3D1-9A8E01D53883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a0e6f86e2688666fdd565b41ef3650ff0bbee40","datavalue":{"value":"certified OS kernels","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$A68640B4-EE7E-4CC9-A6E6-044AE737444F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7d377723b56bb6e951cd42be6b13e05f8af81885","datavalue":{"value":"interrupts","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$E7D6B4C4-6666-4A8F-8C28-CA18E9EF24EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01a9c79fff2a7eb2ecd7e422c08535296f5bec25","datavalue":{"value":"device drivers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$6BE91AE8-87BC-47B2-A95E-E9DE7B2C721B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3b50c1a8989ad8dfe3d1eb03f552830b8d7a813","datavalue":{"value":"abstraction layer","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$6E82E62E-F8B8-416B-ACB3-0BCAFDAEE4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"de7b85c4a93615f621aeed7bf65aeaf693dbddf4","datavalue":{"value":"modularity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1663225$27F68AFD-9D31-4FCE-A2DC-160A9BCB545A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$F502FC5B-93C8-4A6D-93A7-345BE307206C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$33530240-3073-4398-BA9E-70EB232FF902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$FF4C3914-E75D-4BF7-875D-5C56C47A1206","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4feaea7961d9cfdcd7e2968b41cc11ecb0c87f44","datavalue":{"value":{"entity-type":"item","numeric-id":21716,"id":"Q21716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$5978E2CD-4B2D-4FCB-839C-5B095D025F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6cc8b602290f72455ceb0d513144a2973b9cf741","datavalue":{"value":{"entity-type":"item","numeric-id":33310,"id":"Q33310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$1B7F2DCB-D700-4F70-B54B-7D82AAF1FC8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$2E507211-47FD-4C16-9270-2F4D24E9C6DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a1d6b9e920f2e41a66a9767e31ca972ed7628dde","datavalue":{"value":{"entity-type":"item","numeric-id":15668,"id":"Q15668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$D0F9458E-9DC9-48F6-95FB-5E7F7EF92785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$87DE8BF9-F594-4CD9-89C0-F5502B2DFF1F","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$9A447B65-2A0E-4649-AC2F-1C68CDD913C0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8eebc34ef17d880b51f7a3e17021f9c2805bdad5","datavalue":{"value":"https://doi.org/10.1007/s10817-017-9446-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1663225$1D56277D-6F1E-4F2F-955D-68396E3670C4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3b60082680f83770b6c1f3368256bd3af1aff597","datavalue":{"value":"W2781213257","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$F1CFEBD6-3AB3-4D63-B96D-4B3788B044A4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"96c04e68a54aee66416ddeb5ffb45309aa187460","datavalue":{"value":{"entity-type":"item","numeric-id":2829245,"id":"Q2829245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$19939A70-57C0-4FAD-B2A3-2E0C8EB51E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f90f9000203b5cc02cd5a95785f3228e4b1b7c0","datavalue":{"value":{"entity-type":"item","numeric-id":2655325,"id":"Q2655325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$9C52CFF0-FC28-4E64-ADEB-3318F0047C35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec74d20684f0db92c7b7c4239af905bf28ce3849","datavalue":{"value":{"entity-type":"item","numeric-id":1663225,"id":"Q1663225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$B0FF3993-D34C-4E77-AA4D-43909D0B61EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e279107c1bf5c9d2930df902614801cf2fa8b4c3","datavalue":{"value":{"entity-type":"item","numeric-id":1899913,"id":"Q1899913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$7202C730-6BE3-4625-813E-8EA6E75B4DC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a1588eee2e3fe5979cfd18e3e09df49f3b382d9","datavalue":{"value":{"entity-type":"item","numeric-id":945054,"id":"Q945054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$4E09C0FC-0142-4AB8-92AF-A764F92750C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fada031ed317bb64d11da1455ad747b8e2232454","datavalue":{"value":{"entity-type":"item","numeric-id":835764,"id":"Q835764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$052D4D4F-95EB-4A47-890E-AD4D2CA2467C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73901d66c4278581e8cce3d77cced49f915057d4","datavalue":{"value":{"entity-type":"item","numeric-id":2819848,"id":"Q2819848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$3238B8B9-E9E6-4B3B-84AC-A5998821A7D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$B987E0C6-48DC-4CB8-81C0-915FA4F40DCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f7ca9d7d4c37cba35ad27dfba84e476bdb59d65","datavalue":{"value":{"entity-type":"item","numeric-id":5311497,"id":"Q5311497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$5CEE0833-5899-4113-AC62-BAC419D8D7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663225$1FD9DCC1-D981-423B-A73D-0145A3CAE6BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2b0747968e3b75b3a430dd540016e0e41c333c6a","datavalue":{"value":"10.1007/S10817-017-9446-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663225$A0CADAA7-1122-4D4C-B4A2-26461C8630DC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f369d1d1e090ff9d8f9c91135dbf72238a7d4fa5","datavalue":{"value":{"entity-type":"item","numeric-id":2829245,"id":"Q2829245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1246bed4e68f3ced0881a3ceb42d7317501c6d3","datavalue":{"value":{"amount":"+0.7599301934242249","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1663225$0AB0F927-87E7-49DA-9A93-AF498DC7CACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc7146583e41d639c4d4e46f2a3eed6891a858ea","datavalue":{"value":{"entity-type":"item","numeric-id":5477643,"id":"Q5477643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8072d275db3486101edf025fc83c1bc013097ef","datavalue":{"value":{"amount":"+0.7535858154296875","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1663225$A0220987-D9D7-4510-8D24-A84A83ABDE37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ba83feba1be4951b2507336d05662777d195de9","datavalue":{"value":{"entity-type":"item","numeric-id":835773,"id":"Q835773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a15cd32176466c3e516812ce6c37d8aa9577fc62","datavalue":{"value":{"amount":"+0.7498284578323364","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1663225$343A0AEE-144E-449F-B714-6C5994C607AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36ed055ec8f5656036578820cd66c4de107a3a8d","datavalue":{"value":{"entity-type":"item","numeric-id":3067529,"id":"Q3067529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c86eaef31897cefa69b5f13f359b582e8cd94dd7","datavalue":{"value":{"amount":"+0.7450999021530151","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1663225$D023080B-B921-4200-9884-B6F987673B18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983366cc153cae27be16c2535db5be25ad3578a6","datavalue":{"value":{"entity-type":"item","numeric-id":1040002,"id":"Q1040002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c837a026122ad55aa823c344352b383fe083f38e","datavalue":{"value":{"amount":"+0.7372111082077026","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1663225$C0983911-79D5-4A9A-9B32-A5FE93CB73B4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Toward compositional verification of interruptible OS kernels and device drivers","badges":[]}}}}}