{"entities":{"Q5424313":{"pageid":7453887,"ns":120,"title":"Item:Q5424313","lastrevid":92304851,"modified":"2026-06-05T01:23:21Z","type":"item","id":"Q5424313","labels":{"en":{"language":"en","value":"Formal verification for C program"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5208341"}},"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":"Q5424313$947761EA-1722-4744-9CB3-BC70823344E3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"78f89264c95e165b3434e386b5f315f9407b73dc","datavalue":{"value":"1132.68479","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5424313$C6896333-95D8-4BDF-8DE2-B137FBF60048","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b5e1a1f93d0c0634a7ecf5d8b922902097d44856","datavalue":{"value":{"entity-type":"item","numeric-id":2987192,"id":"Q2987192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5424313$89E236AE-E509-48A4-82A1-F4E5D811E753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5cbcf40ed2e7134df6055b0c92761909463e1bf6","datavalue":{"value":{"entity-type":"item","numeric-id":232445,"id":"Q232445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5424313$5510BA83-62AB-4BC4-A46D-2BCE0358D94E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1e1c56210e84f8bb3da2b8d466d5bd545edc9adf","datavalue":{"value":{"time":"+2007-11-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5424313$5768A608-8D5C-474F-B07F-67200E808DB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5424313$CE090F86-3C59-4585-B921-71C894F7DD92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5424313$0ABED9CB-F9B2-4C71-B5EB-95FCD836E6FB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4cf099d699220b17498e2e57d9521cc5981f8933","datavalue":{"value":"5208341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5424313$D6E2EC94-9E79-4158-BAFD-62ABB871A6CA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5424313$47719962-8E72-4085-9609-2A1EAC7AC456","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5424313$0E6C1D71-7C22-45C7-B0A5-5D31F9EEC920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5424313$0EDB48C9-A52A-4199-B7A6-A1AB685180D4","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ad03d9c4dbcdaaddb400f75c486b1d8804afb4e0","datavalue":{"value":{"entity-type":"item","numeric-id":38420,"id":"Q38420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5424313$94FC136E-326A-4F7C-82DD-9E4A49CEB4A8","rank":"normal"},{"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":"Q5424313$77C805D4-4835-484C-BA7D-94EA2729A7D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"47f960de4d53e18e0757a9f17e2bf4db153dde36","datavalue":{"value":{"entity-type":"item","numeric-id":19685,"id":"Q19685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5424313$1D27C5B5-D04A-4C4F-9471-2A1E5EFF9A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc47147a404ecf949cf86c4e92d2dcc5a8bfafcc","datavalue":{"value":{"entity-type":"item","numeric-id":19680,"id":"Q19680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5424313$EAE6B65D-C2F7-4A34-A8DF-DB258BC5EC37","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":"Q5424313$0E173CB8-081A-4DD9-B77A-5DD2C76F57D4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bd71d433d357833a1ab35135bc0074a796311f9","datavalue":{"value":{"entity-type":"item","numeric-id":4414373,"id":"Q4414373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a90fc4bcabf531e57c8dfc55015f552307a2d1f","datavalue":{"value":{"amount":"+0.8165201544761658","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":"Q5424313$6570FF04-A432-439C-A86D-A4A47BB2D5DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85ebbee7b7abce6bc9db7943aebd0d1ded4c399e","datavalue":{"value":{"entity-type":"item","numeric-id":1888200,"id":"Q1888200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b415e9b2727aef7130c4ad9e1474980926df11d","datavalue":{"value":{"amount":"+0.7969295382499695","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":"Q5424313$DEF2ABF2-714C-41CD-A3C3-A40C5489F2F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"609db31109f29daf5f20500cb6e669dae387d5e6","datavalue":{"value":{"entity-type":"item","numeric-id":5902361,"id":"Q5902361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f454a7fcae7eb579c231df0956356ae8121625b2","datavalue":{"value":{"amount":"+0.7820071578025818","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":"Q5424313$3B1FAE43-EDC8-415D-9BEF-BAB7BFC5AD1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bac9d4d28f254e49858c9874367df8c34d82c78","datavalue":{"value":{"entity-type":"item","numeric-id":3176373,"id":"Q3176373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e8243617acd695d743ca579348948164b2175f6","datavalue":{"value":{"amount":"+0.7782095670700073","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":"Q5424313$97512698-AE37-42A2-8B43-A10F5F7CE2FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a76b3577a7618bb02f9806580f51d2b7da93b94","datavalue":{"value":{"entity-type":"item","numeric-id":5900551,"id":"Q5900551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0a5fb563295d5f13fb7769fab252b6a94d8c2ce","datavalue":{"value":{"amount":"+0.777184009552002","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":"Q5424313$00C7E603-CB71-479F-857C-044BAFB0299D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal verification for C program","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_verification_for_C_program"}}}}}