{"entities":{"Q3543656":{"pageid":5573560,"ns":120,"title":"Item:Q3543656","lastrevid":50516516,"modified":"2026-01-14T06:35:00Z","type":"item","id":"Q3543656","labels":{"en":{"language":"en","value":"HOL-Boogie \u2014 An Interactive Prover for the Boogie Program-Verifier"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5378179"}},"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":"Q3543656$5DC00A81-D03A-4FB2-97C7-EBCE52F9F77E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f46f1b17be43434c3d8de3b8472fc706f2f1c46f","datavalue":{"value":{"text":"HOL-Boogie \u2014 An Interactive Prover for the Boogie Program-Verifier","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3543656$2CB5494E-882B-417B-A718-26D155180E21","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"44c7febdf9e3d096a0b3b45b9c09a879fd650a28","datavalue":{"value":"1165.68399","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$C118BB58-2483-4B75-ACFB-E985FCB614C1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"089753c6c5f083d31c3593742269880ad8a6c62b","datavalue":{"value":"10.1007/978-3-540-71067-7_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$7D06DA8D-B38F-49DA-BECF-3A9AB37E09F8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e52ea9fecc32655489a0560f1f3a2c96d34140f0","datavalue":{"value":{"entity-type":"item","numeric-id":287336,"id":"Q287336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$129AD304-0079-429F-BC7F-36D798C51A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f4e0c2c58ff8fd4ec1edd435e868f3bbbace9fa5","datavalue":{"value":{"entity-type":"item","numeric-id":633284,"id":"Q633284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$FA97FEA3-34EC-4851-925A-CA3805B3B42F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"21d75dcb945540c248584601b42ebed5a2d66b5a","datavalue":{"value":{"entity-type":"item","numeric-id":470024,"id":"Q470024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$02F5F729-6EC6-4BBF-843F-30C4AADEC067","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$BE9D576D-3283-4F9F-B527-348E5A290EE6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9390341f6bd0adb4a80933997da5182af87828a8","datavalue":{"value":{"time":"+2008-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3543656$E9D55104-4E24-48A9-81AA-A5248F6E4382","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$632321D1-6DC8-4FD1-B932-25DD419CA1BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$EBBD18BA-A9E8-465E-B365-C2393128C4AF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ce5147886edefb27dee203608e1b6c7d89a8705e","datavalue":{"value":"5378179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$B05DD219-CEAB-49B4-BED5-42AF522E3C86","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$C7058F4F-4623-4247-94FC-C72A9EC09AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$12FC3164-E17A-4016-8420-25D9AD5AD180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8312fa7309b2bb86919d80d9dd327b01ccd3eb19","datavalue":{"value":{"entity-type":"item","numeric-id":19268,"id":"Q19268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$D76E1CC0-8B9F-4FED-BA8A-0656FA920AF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$A9F140FE-F3CB-4ADC-8EF1-EC440FE8C553","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$5839C2EE-3B41-4A53-9D41-31F0F212547A","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":"Q3543656$155AB5BF-23E8-4BB2-B172-7A1C1F0443EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ea1fa890b2f09c8cd0bccb17957cf46696afec2a","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$1C18B6AC-132C-4EF0-88F7-0208F7DA470E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fe5077d712c4f7a91829b6a22ef0e0039cd600ea","datavalue":{"value":{"entity-type":"item","numeric-id":15691,"id":"Q15691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$BFB79C5B-6675-401B-A1BF-ECADFA29DD4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d560ad72fd288969b6a46f8ac77d54f6d297bf97","datavalue":{"value":{"entity-type":"item","numeric-id":16796,"id":"Q16796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$7F772A83-0712-4476-B9AA-56C9278AB9ED","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":"Q3543656$AA432E57-B059-4BB4-A5D4-246EBF5C1611","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"93403021c48a812d9127910dbcaae98db02c160e","datavalue":{"value":{"entity-type":"item","numeric-id":33328,"id":"Q33328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$F10F3192-D009-49C6-B11A-CF779BACBD52","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":"Q3543656$68D76B6D-982B-49CE-96B2-96D5A241EBF1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0559b57864b2fad124cf389d1f55c09a289bc1d7","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71067-7_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q3543656$B5ADA5FE-F849-4A52-A420-5859B00448DA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3cf3e706712706a2fc0d9705d10abf1d25c1dca1","datavalue":{"value":"W1515169568","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543656$9AF9FDC1-0B07-46F8-8A3D-6F47C0D4C82B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0482a84e9c0157add273943bbc51321d78bf5bd","datavalue":{"value":{"entity-type":"item","numeric-id":877156,"id":"Q877156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$CA5B4FF6-00F7-4091-B4A7-F1D261CD6C56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c12869f31923e79c52c725d24c081909254f4f3d","datavalue":{"value":{"entity-type":"item","numeric-id":1776586,"id":"Q1776586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$FF39E2A8-8884-48F8-886D-92D846C43464","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30331b0843d8fad412757315603331be3191b0d9","datavalue":{"value":{"entity-type":"item","numeric-id":4711615,"id":"Q4711615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$61787BC7-6C2C-429C-9DB7-BD707988D9CE","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":"Q3543656$B187048F-0B3C-4ADF-A8E0-4E16BCD1838D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3f0c070d63cc8ade73e849526c8ff12c4b898b","datavalue":{"value":{"entity-type":"item","numeric-id":3523187,"id":"Q3523187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543656$CE97AFDD-9BE1-4E08-B559-E6715175DA27","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e62cbe64cfa326fd14d664e2324b4b583ba4a98","datavalue":{"value":{"entity-type":"item","numeric-id":2655335,"id":"Q2655335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acb0290a6d08b80eaecc4a50da7def1627e345f6","datavalue":{"value":{"amount":"+0.9574667811393738","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":"Q3543656$FC6E6CB2-18E0-42A3-A42E-B6B5387D9E2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"207c31bc4ac70f3a4595fb667a52ca7b1945ec0b","datavalue":{"value":{"entity-type":"item","numeric-id":2102933,"id":"Q2102933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b06ab83983f623fdf9963faf7568fe5373a26182","datavalue":{"value":{"amount":"+0.7756077647209167","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":"Q3543656$2A712FA5-42B5-41BB-A759-A4ED22B7F1D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2329ac48b709f66aa4e2a0cfdaaaf3d4cea285dd","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a89b402bb560beea317366d798550d37422730f1","datavalue":{"value":{"amount":"+0.7457154393196106","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":"Q3543656$A6954E12-A763-4932-961F-01BD8D8198F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ddfe8706eb56f964bdfd12380be6a420c1d49e0","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64b26b9ca0f962e516a95886e97445480e9cc6cb","datavalue":{"value":{"amount":"+0.700526773929596","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":"Q3543656$F1AD2625-DC0F-4971-B19F-084A4CD2155B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9c2bbb3df2b96668f129f74b95b0e10b1d032e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326280,"id":"Q5326280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ce9e357c26890d64b60ace7501d446cd9278e1f","datavalue":{"value":{"amount":"+0.6941956877708435","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":"Q3543656$5AB52F5B-05BD-4642-9551-CECB9B45E12D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3543656","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3543656"}}}}}