{"entities":{"Q835773":{"pageid":837621,"ns":120,"title":"Item:Q835773","lastrevid":64732215,"modified":"2026-04-11T21:51:27Z","type":"item","id":"Q835773","labels":{"en":{"language":"en","value":"Formal memory models for the verification of low-level operating-system code"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5600121"}},"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":"Q835773$FAC2ABB9-FC3A-4D7C-AA63-3D9C2CD2B658","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"214ebce611e3f4b305ae65dc7cc2659fb7d5537d","datavalue":{"value":{"text":"Formal memory models for the verification of low-level operating-system code","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q835773$15300FFE-5F1E-4397-873D-5FD311893731","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9e24308bcdd618a1ae0958325da4c47593789de0","datavalue":{"value":"1191.68178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$FB912255-B055-4929-B94E-EFB869ADBE9F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6997ab07e7932b481a649bf1d5271ce569949f23","datavalue":{"value":{"entity-type":"item","numeric-id":835771,"id":"Q835771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$03B23CB0-CCF0-4F37-BEF5-6EFC24509ED6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"294fd8051deb8524fd06e56188039253c095891d","datavalue":{"value":{"entity-type":"item","numeric-id":835772,"id":"Q835772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$30068F59-7C11-4815-A7C7-0C04BAEDBDCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1f8cd3b806fd78547b3f4844ba487e41a5ec455","datavalue":{"value":{"entity-type":"item","numeric-id":286783,"id":"Q286783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$A2F00C6E-2387-4C3A-AEA7-3FFCF81BFFA6","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":"Q835773$5DD8974C-09BD-49A8-A14D-9639F4116F60","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"049debda757703127da2fc03ca0a1b5b826f121d","datavalue":{"value":{"time":"+2009-08-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q835773$C8E92E84-9A56-40D4-94AE-6C15ADB6E35C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$31F82EB9-7345-42E0-ACF0-EBC692D60092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$4BAB23D6-2512-4A41-8068-17A1C6E04CCE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"27731ed2e0ea84d0728626ff2aaa99f2b5bd7792","datavalue":{"value":"5600121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$F7A87F53-9164-46C3-A9B3-03F99AB03441","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4411819ed476665944e8ed7f31668a3d637f53bd","datavalue":{"value":"operating-system kernel","type":"string"},"datatype":"string"},"type":"statement","id":"Q835773$34C0964D-C34E-4B03-B61B-308B61B511CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e843101ef2410398de55bcd0cb8ef16af7446f16","datavalue":{"value":"micro-hypervisor","type":"string"},"datatype":"string"},"type":"statement","id":"Q835773$F57ADCEB-1248-4E99-BCDC-A5D7B416ABA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61f64b4290cb6eee91e383d71c1245fa4a6d4624","datavalue":{"value":"virtual memory","type":"string"},"datatype":"string"},"type":"statement","id":"Q835773$6EECF275-DFCA-4D2C-9531-D6A54327B39A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"49d78eb5ebc5e0530cda91785f90e2d5cd42541f","datavalue":{"value":"memory-mapped devices","type":"string"},"datatype":"string"},"type":"statement","id":"Q835773$9CC6837F-33B2-46BD-A7D0-7E52B1D8D57A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q835773$B13A1CC5-5365-472A-BDA5-A19E16A518D5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$15EEA900-6ABD-4028-9DDD-71FB16CED198","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bee5cb1919919ea97c6e467c1806a0893670d996","datavalue":{"value":{"entity-type":"item","numeric-id":14223,"id":"Q14223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$C7FD063F-B880-44EC-89EC-8AEC0D65D78F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab1d940260f20d8e15c2593184ef71f159cef550","datavalue":{"value":{"entity-type":"item","numeric-id":34113,"id":"Q34113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$430B1ADF-F860-48DE-ABE2-887D9C86ECCC","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":"Q835773$F6DA7842-B57A-4BB9-B3DC-6E4CF1C70B2F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc89c7839faeabb3424b2f018c68246490f71453","datavalue":{"value":"https://doi.org/10.1007/s10817-009-9122-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q835773$6772B7F6-317F-462E-B396-61B2B42DAD3E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7b707ba8bb3d710e1b9f863273fda14f9647093f","datavalue":{"value":"W2104622601","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$0E75355B-992C-491D-B508-13F4209991A4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f1461786fd9147b7231c61e645f0ab20a3eaa42","datavalue":{"value":{"entity-type":"item","numeric-id":1040002,"id":"Q1040002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$90DFC521-11FE-400D-98E1-53852E03D1E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ec976db9fee9bededf233dd7d31c7e9ef2213c8","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$15A9FF51-63B9-42A7-88A5-9652BCBE6EA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c07a28c7e7e5c427d56d83fba3f415dd8cd71a73","datavalue":{"value":{"entity-type":"item","numeric-id":5387859,"id":"Q5387859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$F5F67552-DE37-4DA9-9205-BF38F0089599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19d68f92fffaefe72b592d24843b2770631f989c","datavalue":{"value":{"entity-type":"item","numeric-id":3189788,"id":"Q3189788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$D40E72A3-C76C-4053-B711-8A195C87FCFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60b38947aa70ea970521d878b67d07ff7c71b08f","datavalue":{"value":{"entity-type":"item","numeric-id":3863057,"id":"Q3863057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q835773$FCF14310-9A07-4036-B21C-98AA872A39F8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0c92a8fcca727fc1c19c8f3a5baee8565f27f0ab","datavalue":{"value":"10.1007/S10817-009-9122-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q835773$76AB8D7A-0937-461E-8443-FADB058254E8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efe92806a81bbea1cd5444ec3bcbd3de48fd0186","datavalue":{"value":{"entity-type":"item","numeric-id":945054,"id":"Q945054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfcae599076957959b0be7837133cb1be46ac412","datavalue":{"value":{"amount":"+0.9238311","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$379F5BDE-6FF3-4D95-BCDE-EF15C592B829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c86587f2662a09c87989a48ab7311f9208b8e337","datavalue":{"value":{"entity-type":"item","numeric-id":4412529,"id":"Q4412529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c5174d4c74be9dbe4af3daa9232405cad5df68d","datavalue":{"value":{"amount":"+0.9171059","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$15F98395-426B-4AF2-A4A4-21734C37FDA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29e044563e77ff239ff7b9add1b9c2e22a0ee351","datavalue":{"value":{"entity-type":"item","numeric-id":5897064,"id":"Q5897064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"baa2586d429eee38ed109a091f7f79dbad134eca","datavalue":{"value":{"amount":"+0.909023","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$C9517531-659A-4C74-AEDF-166ED98E771D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53389ff29cd92def7f542c1a68c503dc45db02e7","datavalue":{"value":{"entity-type":"item","numeric-id":3512487,"id":"Q3512487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ee87537d0abc8e6899f6970e945f739e6e641a5","datavalue":{"value":{"amount":"+0.9014471","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$B8B0E515-87C4-43FA-951E-5E0CC727DBC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f366e5466d4b0621aaf9bb2b1370668cd91fe511","datavalue":{"value":{"entity-type":"item","numeric-id":5493234,"id":"Q5493234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0aed31be5bf08e1758466971feb3c60425db727","datavalue":{"value":{"amount":"+0.8931306","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$2D24D695-E1FC-4C53-AEEF-612390570B8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920846cee47ebcd0c156e2badd883856874915ab","datavalue":{"value":{"entity-type":"item","numeric-id":681346,"id":"Q681346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d8797b294d2f04e033d9dcfb7ee0044626187d4e","datavalue":{"value":{"amount":"+0.88819194","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$B4F5714E-322E-4E5C-B608-58D782EFE4CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5beef82811c1ed410a89dd64b21f082cf77902e7","datavalue":{"value":{"entity-type":"item","numeric-id":5172657,"id":"Q5172657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d8797b294d2f04e033d9dcfb7ee0044626187d4e","datavalue":{"value":{"amount":"+0.88819194","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q835773$BC8BCE8B-BFCC-479F-9B37-1814213218D1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal memory models for the verification of low-level operating-system code","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_memory_models_for_the_verification_of_low-level_operating-system_code"}}}}}