{"entities":{"Q945054":{"pageid":946902,"ns":120,"title":"Item:Q945054","lastrevid":65534550,"modified":"2026-04-12T03:16:19Z","type":"item","id":"Q945054","labels":{"en":{"language":"en","value":"Formal verification of a C-like memory model and its uses for verifying program transformations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5324393"}},"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":"Q945054$59E272BB-6DA0-4271-8CE2-9E7D355BC762","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c6706e51eb48ce9a394a3cc4eb92f8a9c41f4bef","datavalue":{"value":{"text":"Formal verification of a C-like memory model and its uses for verifying program transformations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q945054$55DD5272-9653-4CBF-BA4B-F908CA4532BE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cbd66477c06dfe9f81c0b55c4a84759db29e4c17","datavalue":{"value":"1154.68039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$089CEBE4-5A13-482C-88B6-5E69E0D693D4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4b1e35c1c4bff0a8e8e775e8600e2e952b118ae","datavalue":{"value":{"entity-type":"item","numeric-id":848738,"id":"Q848738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$F0F103E5-B020-47E8-A212-272A9011E22A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5f71649d5cd536e6a70ddc24feda92d797a4529b","datavalue":{"value":{"entity-type":"item","numeric-id":287366,"id":"Q287366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$115DBC4A-92C4-4DC6-8E0A-B8FE67049138","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":"Q945054$7AFBD323-91AC-4E2D-9FEB-79701BC963D2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"131b596fa601c3661806f2437747b7af2f563219","datavalue":{"value":{"time":"+2008-09-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q945054$F68755AE-C29C-4DCB-A726-4E364BE962DD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ddbf57a48793d9b33eb2f946f6e963ca5e342a4f","datavalue":{"value":"https://hal.inria.fr/inria-00289542/file/memory-model-journal.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q945054$BE18556F-3594-4D2B-80E2-A05AFA7CC675","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$A76C833E-AF8C-4828-8535-26F74AB0A48B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$15AB31FC-9271-4A19-BA83-47B50A9587EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$C442F747-1452-42EA-AD3E-9D4831E8DA7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$F3F93F0B-6AD5-42B6-8D94-C37E10453E8D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f31e476f6812350894c1251501c21fca7a3e4503","datavalue":{"value":"5324393","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$C8B8DE6D-CE84-495F-A5A5-2B5C5643F9A3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa69173775bb221301a9371f987089aafe188951","datavalue":{"value":"memory model","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$7676F8A9-3D05-4946-849D-0CC1AA62A628","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95f35984d75f96b8273ee58ad427140a23f29b8c","datavalue":{"value":"C","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$0F39F384-6134-4387-8B9C-37E7333A8AE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$CACEF7AC-EDDC-4415-89B9-278FEF1AD472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30465c7253323499b5cce6c4f064def1ef2d4445","datavalue":{"value":"compilation","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$1FF0E818-08CD-46E2-AEAD-89E206F71694","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d958ef02bdf074a60d670471cc677567c94c4a3","datavalue":{"value":"compiler correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$948F50A6-294D-4A43-B0E8-1004E78DB1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98456cd4cdf0db037b678749018452921ff9260b","datavalue":{"value":"Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q945054$46AC5CD2-567A-466A-80DA-C43DDB10AACD","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":"Q945054$206CD33F-29A1-4AEB-A731-E6AE0AFBF4FF","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":"Q945054$88C758CC-8FFB-445A-8938-529A379AAC49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"328a4887d5a745918f682c9b5cd832468b1041c7","datavalue":{"value":{"entity-type":"item","numeric-id":21718,"id":"Q21718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$B637DBD6-E59A-48D6-9972-9E7E4FAF0193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0e0883f941bb980e3b01a34d83dd8c3a67055c8c","datavalue":{"value":{"entity-type":"item","numeric-id":22100,"id":"Q22100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$1DEDC5DF-F87B-4ACB-9F8A-4CE7A4AC66EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$F55D2E93-76A0-4708-AC46-053019B9A978","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":"Q945054$A3E9C734-5472-419F-A343-E9608796963B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3bc55246e74ea553b217d4851d3404dbec7a30f7","datavalue":{"value":"W2154942048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$2D3254A8-E7DB-4D66-B49C-A491BAB6D2B9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ed5124fab1d64feb8b4feb25646b660a09eb4cd","datavalue":{"value":{"entity-type":"item","numeric-id":3523161,"id":"Q3523161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$C483A359-9588-440C-A051-5CCE23C2E751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$2A9F0A95-B694-445B-8091-75A332D276E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"288e9539ed7661e715c4eb9511317e6936f53231","datavalue":{"value":{"entity-type":"item","numeric-id":2721096,"id":"Q2721096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$DF24C601-9283-4CE9-B397-8D7D41FECE81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16df2553495bc38f714aaa2197b34e11b69c06ef","datavalue":{"value":{"entity-type":"item","numeric-id":5674963,"id":"Q5674963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$EA7D7926-E2C4-402E-A6AB-34C114338BBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$9E2C3DC3-AF31-4EA4-889A-4E0B11362A4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07e1822cc4b1e1be7d3f6478fe3be7e4f705bee5","datavalue":{"value":{"entity-type":"item","numeric-id":5899013,"id":"Q5899013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$AE3C2C36-EF4C-4A0E-B127-1EAFA67132EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$BF3104CE-F2E1-4920-A961-F24FAC83E686","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aad708b8e4e30e35c3846234774de37622f45350","datavalue":{"value":{"entity-type":"item","numeric-id":5276162,"id":"Q5276162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$495D4151-A976-4F3E-AFF9-2EBDC5914643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3be8c8d124a78b7bc05b7543e4a39424af55fffb","datavalue":{"value":{"entity-type":"item","numeric-id":2486585,"id":"Q2486585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$2A5A956F-B36B-4DBF-95E5-519E01F45A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"135d76ceaca9cbc58259ce94329d287fe57a3fd1","datavalue":{"value":{"entity-type":"item","numeric-id":3189840,"id":"Q3189840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$7743E8EC-8417-4F3A-B18F-5D955DA5AD66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb5c384f83cfe304bd792549ed6786939a461655","datavalue":{"value":{"entity-type":"item","numeric-id":4783297,"id":"Q4783297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$6C463930-286D-43A4-975B-5DEADD5DB00B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e2ddce7deb9349ba26913c3b88a9d05ce8d4139","datavalue":{"value":{"entity-type":"item","numeric-id":1566883,"id":"Q1566883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945054$45584EED-A060-4E97-A618-7FF3BF166A7A","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":"Q945054$41506ACF-83D2-4356-A00F-CBC1B15C5B30","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d6e9f6aa924a5746adf760831914e1cc08ab9adf","datavalue":{"value":"10.1007/S10817-008-9099-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945054$4F4FB59C-8780-4371-8C26-EC55E5705540","rank":"normal"}],"P1643":[{"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":"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":"Q945054$C7E428A9-E8EC-4ECA-8625-F5043605DF8E","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":"99f036ee310758c690aa7a99e58fb786c49f15ab","datavalue":{"value":{"amount":"+0.89621043","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":"Q945054$973C04B0-3BA1-48C1-85A7-266829A5C4BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"955e861e1fd297cd8cc3234d45c6ea1f53c2ee3f","datavalue":{"value":{"entity-type":"item","numeric-id":5326305,"id":"Q5326305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56ba898994fa9587fc365bcf7baec701185cf2f2","datavalue":{"value":{"amount":"+0.89355326","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":"Q945054$FA26CB9A-370E-436B-A52C-1F4378961BE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1294c4fa2a4e90c4632fa3ba78297f983342db7","datavalue":{"value":{"entity-type":"item","numeric-id":2988675,"id":"Q2988675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52a5a7ccb61217c0bd9836e78f328cc8f43eb3d6","datavalue":{"value":{"amount":"+0.8878424","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":"Q945054$1C909583-296A-4D4A-B83C-0EA3269820FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c334e8232bc5ad004702c67c08ebf996e4b8acc","datavalue":{"value":{"entity-type":"item","numeric-id":2912700,"id":"Q2912700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02a8125cfc0f98a2347283e593ecaeb3b5902122","datavalue":{"value":{"amount":"+0.8878347","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":"Q945054$7E1A9E93-2453-43A5-B27B-703DC327D0A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"573201f06fe9b16eb9dc3d33f5d647a5d78f5831","datavalue":{"value":{"entity-type":"item","numeric-id":470040,"id":"Q470040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c29b98dd783a11772639270cd78f3668988ff44","datavalue":{"value":{"amount":"+0.8853916","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":"Q945054$E92AB6CB-B7A2-4B66-B41B-78CEA1BBC860","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":"f9583fcbc7486e3987b85648f6b5430ab3cc41ed","datavalue":{"value":{"amount":"+0.88402164","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":"Q945054$CBDF6812-CB16-4782-ABCA-06C52443FF0C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal verification of a C-like memory model and its uses for verifying program transformations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_verification_of_a_C-like_memory_model_and_its_uses_for_verifying_program_transformations"}}}}}