{"entities":{"Q5056076":{"pageid":7085653,"ns":120,"title":"Item:Q5056076","lastrevid":91921910,"modified":"2026-06-05T00:24:53Z","type":"item","id":"Q5056076","labels":{"en":{"language":"en","value":"A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7631593"}},"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":"Q5056076$DC654700-7C49-4BCD-9E08-F19F622C6739","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"57b5db60ad9a66ce036e948016fd9f2252a22bf0","datavalue":{"value":{"text":"A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5056076$18F40ABC-B830-450B-A2EE-014F851DE259","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"28b3fa2e469039d8ef2ba3fb8fe731d7ee576636","datavalue":{"value":"1504.68037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$1D547C67-469C-4012-874C-9A24BBC37168","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b2369c39805b1f73b3e52077b0f1856bda790e66","datavalue":{"value":"10.1007/978-3-319-90104-6_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$5FC52D2F-719F-495B-A4DA-C76F987E8B01","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ffdbc0242d92de16fd8d8a6a20f7780d8c4aea1","datavalue":{"value":{"entity-type":"item","numeric-id":5056074,"id":"Q5056074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$B6AA970E-A9E3-4FE3-8947-F7BE348D3B0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0a2361c47e9a88dec1b4d417725037c3ebace4af","datavalue":{"value":{"entity-type":"item","numeric-id":5056075,"id":"Q5056075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$45B549D6-8793-4DBD-892C-F5B05411EAA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"19c8b8152eb049581c2538d13b0e2ff0fba8e40b","datavalue":{"value":{"entity-type":"item","numeric-id":520242,"id":"Q520242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$387D1782-59E2-407A-8C0F-105E9B936EC0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"46c13b4ed20d7be55f678f5b2789c4af66377d94","datavalue":{"value":{"entity-type":"item","numeric-id":4989013,"id":"Q4989013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$B60790F3-BACA-43EB-85DE-0F848EA290CE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"11447fc0ad9bdb1f5ac45f1763d7f4fd1b0676df","datavalue":{"value":{"time":"+2022-12-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5056076$5CBCE46B-B2E9-4D30-B651-B77594EED93B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$842CA4A9-0D97-458E-81DA-3406CA85A6C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$6C95D37E-8F37-4353-B594-80EEC6ED634B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$199E3C63-D2E9-4B20-99F9-D86E10F9EAE5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4c9d9731ceeee12ad129b335dc10027d5e6f8406","datavalue":{"value":"7631593","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$F6BA2D2C-81F2-4538-93A0-4ACF18C5CEF1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47aefda07ac5d6e74103bdf2455b1df41b0e324b","datavalue":{"value":"algebraic specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$CF1EA37B-FDDB-493D-A793-02A4715EBB1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b9774ec536a335bf339af8b08118f8757f918204","datavalue":{"value":"CafeOBJ","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$ABEA150B-D79B-4E5C-8F99-8D5D02FCB690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"901c6d511d35303a6a968c1174234f4350020c8b","datavalue":{"value":"compiler","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$90199A5D-0E87-4667-B221-C27131D7675E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$06BBD288-34B4-4F4A-A918-B098BCECC8E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d31b0b7476ae8e41dd75304ca63c96200ee6c96","datavalue":{"value":"proof score","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$BD386ACD-20DD-4CCE-8E24-390778BE21CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056076$F9DC7DE6-E94D-49C9-9626-35451CE21777","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9cc08f1ee64c2fc0d984a8fe54c7c857eeb0cc4","datavalue":{"value":{"entity-type":"item","numeric-id":18366,"id":"Q18366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$6595B35D-7E17-4BBB-89D4-D8750F4FE394","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6b3dc99177236f98a28268bc9de8552588fda1ec","datavalue":{"value":{"entity-type":"item","numeric-id":30822,"id":"Q30822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$2C6474C3-7137-4A6F-9FEE-A59C4E0A2B1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4840352b17217b124b50c88ee4bd6bcc958c902f","datavalue":{"value":{"entity-type":"item","numeric-id":17510,"id":"Q17510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$AB4094BF-E08C-4E5F-8B1E-F551158A5EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a7e8c0ef4b2b655550f401b23c169644988922e0","datavalue":{"value":{"entity-type":"item","numeric-id":21725,"id":"Q21725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$FFA4642F-DE2C-4AF4-9404-8AA92DB88FCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$67C8D026-439D-4514-BC44-265D9E3097D5","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":"Q5056076$7B9CF171-5B14-46A5-884C-D3AD0DD9838F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"50367928f9277bb925a8abdb06ed2808c2396f3f","datavalue":{"value":"https://doi.org/10.1007/978-3-319-90104-6_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q5056076$4BE47505-D869-4176-AD15-4A97F6321B90","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a1d0e9f9c4ebb498f87d7dc2bdbcb171ca031383","datavalue":{"value":"W2798751341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056076$4EB543D2-8F6F-4925-9739-4DA37252D105","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"685b6f2241ca731964008614149743ea5d098bf5","datavalue":{"value":{"entity-type":"item","numeric-id":2715825,"id":"Q2715825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$6424C73C-B60A-4AC1-9299-8161B9221AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9d81257f3403e2bd6dfaf12e4319d6962382d0e","datavalue":{"value":{"entity-type":"item","numeric-id":5096184,"id":"Q5096184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$7AD69733-A891-423D-A45D-46983EBABA87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"333782dfe2a782886768e8c7561d4e8bfd035e1a","datavalue":{"value":{"entity-type":"item","numeric-id":2655327,"id":"Q2655327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$DBEB3D13-E276-473B-8F87-5918D0445FD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c730e7a11765d2866ae1e1a84de71868633eeff0","datavalue":{"value":{"entity-type":"item","numeric-id":4346205,"id":"Q4346205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$710BA9B0-E2FD-4B86-9B00-574EA15D0078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23623728af77877c2c658b5f16ea2ac66fec79f9","datavalue":{"value":{"entity-type":"item","numeric-id":987974,"id":"Q987974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$0B2E6D25-9D52-4FF3-AC55-6BC5C3B8F8B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2a7a357eb6113b166cb4bb85e076f679569ab25","datavalue":{"value":{"entity-type":"item","numeric-id":2819831,"id":"Q2819831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$09950A7F-7D6F-44C2-8A5E-AAF40E6AB453","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69bd394a77de6a66e7c3ead14354e268bd49cc00","datavalue":{"value":{"entity-type":"item","numeric-id":997833,"id":"Q997833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$D586E11C-ADDD-423D-B46C-6CF0E488D8CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"660e372c2fab9f49c1eae2ff439d4932a3c2a6cd","datavalue":{"value":{"entity-type":"item","numeric-id":5411641,"id":"Q5411641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$321C9C6B-7B63-4F03-A487-BA568170D673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c0b8cbc0550b2f8905e471ff15c76bfd64ad0a0","datavalue":{"value":{"entity-type":"item","numeric-id":1575735,"id":"Q1575735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$5C02FE74-DAFA-43D3-997E-D64196604080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e46aebc04c4ba0e79011f44184decc8d5c2923","datavalue":{"value":{"entity-type":"item","numeric-id":4520814,"id":"Q4520814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$E036A206-5FFF-4721-9709-45DA9E7DFE07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"211eb911509defcf3cc735956cc564f8ce863a20","datavalue":{"value":{"entity-type":"item","numeric-id":4809043,"id":"Q4809043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056076$312952A4-2BF4-4C23-848C-2520EAB5FDF6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc642dbdc28b23eb9dd71b8412c41128d8900904","datavalue":{"value":{"entity-type":"item","numeric-id":4809043,"id":"Q4809043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca3f607b6c70c12ea7c133726c5b4a0283608f64","datavalue":{"value":{"amount":"+0.7704432606697083","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":"Q5056076$54D82DA1-39CA-4F65-8179-86A0C679BA6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f29474da1eb824221d8a9a3b9e4e3876194dc88","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48e45c215c05013fd93dcba9f6ab52e90010d7d1","datavalue":{"value":{"amount":"+0.7530509829521179","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":"Q5056076$9E401639-AE2C-4ECA-A2D5-68D789B9564E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"177a6e4ae87fbc69cc049e90a51aef2ccb197c87","datavalue":{"value":{"entity-type":"item","numeric-id":2655327,"id":"Q2655327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35f4b9684bd627a7aa6100f1e329e6fcb31601e5","datavalue":{"value":{"amount":"+0.7512044906616211","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":"Q5056076$0C687A9B-3518-473E-86AC-50ABF2B60C3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a78656e009a875f791fb00201d65f8f9e3e67b0","datavalue":{"value":{"entity-type":"item","numeric-id":3200537,"id":"Q3200537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"708aa9ec4f7819d4c4cce712d3118ca28b6cd9e2","datavalue":{"value":{"amount":"+0.7362141609191895","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":"Q5056076$5ADBE2FD-F83C-477F-B224-FA33BE961E08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04d5a3ac333c1f515b93cc74ab7c13c8aed9af4f","datavalue":{"value":{"entity-type":"item","numeric-id":3615276,"id":"Q3615276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9259c903f2c908d71721eadf537f4c154f42104","datavalue":{"value":{"amount":"+0.7235605120658875","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":"Q5056076$FCF5ECDE-D93F-4B3A-95AC-44C76E73D78D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler","badges":[]}}}}}