{"entities":{"Q6156936":{"pageid":13291511,"ns":120,"title":"Item:Q6156936","lastrevid":41642001,"modified":"2025-05-06T16:21:27Z","type":"item","id":"Q6156936","labels":{"en":{"language":"en","value":"A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7697494"}},"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":"Q6156936$07B71153-CA0A-43D3-9A55-CFC52D286A92","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7b4baf34356d19b66d7b4aeeab375c8dda4b400b","datavalue":{"value":{"text":"A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6156936$BEEFB057-3A27-4A29-B704-CE5D64DF60DC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"09dab8c34a6400903af586b001654d10d80c9879","datavalue":{"value":"1512.68151","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$85D97018-44A2-4CF5-8736-D0569ACD6BC8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a4d4f10eafc7166d616956f86ea8b4213ac9879","datavalue":{"value":{"entity-type":"item","numeric-id":1960261,"id":"Q1960261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$B3E33A08-BB13-402A-9062-867A0DD3053D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b22589ac4799fa11bdf6a319668e8a088247d277","datavalue":{"value":{"entity-type":"item","numeric-id":465684,"id":"Q465684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$53D756BE-9B12-4880-8B5D-02693F9FD259","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$CDA9ACE0-1608-486E-BC91-EB6EFCA1D827","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1568bcdbc15a3da62bd02289f2e9e5d50d8fef1d","datavalue":{"value":{"time":"+2023-06-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6156936$5F36AA98-C74A-42D1-98DA-024D57322FAB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$9E21A90F-7A5B-4BD9-91B4-9115B7727299","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$8F320D9E-216F-46CE-9E18-EE44B0715CA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$A1D6FD8C-924F-4F42-AC7D-9D51198CE6F0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"06843f1c384ac120cc2525503ac3bf523d7a9e84","datavalue":{"value":"7697494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$309510A9-2BF3-47D7-8463-B62B77577AD6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$A1D48AA5-B692-46DE-B3CE-6CB888114362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c466a31828be4527e6fa92732efebe73d5786789","datavalue":{"value":"verification conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$EC0509C7-0C27-4462-B5D0-530944328ED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$7DB56534-9CAB-4E92-8A99-125D01291A2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a659848b6beeb7408fc636bba8858d3222f4002","datavalue":{"value":"program annotations","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$EE58BFD2-4922-4FEE-BEF9-22257D467A76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"199c60de1e7b1805727a447210896226c6321a81","datavalue":{"value":"weakest preconditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$A44C756A-5159-4790-93A7-9C27C9C36903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7beade670f98ecc34df2f1ab9c90a695626f86b6","datavalue":{"value":"updates","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156936$2DA4A370-88EB-44D9-8BBE-DCA3F2F1445D","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":"Q6156936$6A87F30E-C5A2-4004-8153-CF202D116E92","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"65fd32c7f6f8f566e74e5a64c904e6c8fdc2b82c","datavalue":{"value":"https://doi.org/10.1016/j.jlamp.2023.100871","type":"string"},"datatype":"url"},"type":"statement","id":"Q6156936$18AAF5BB-B33E-42AB-BEB8-90370B2011C1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b5e650d9914bdc45d8661a9b5c97b2a8a9862bf5","datavalue":{"value":"W4360999344","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$43B841B0-8D13-462C-BD7B-76F47C43F4DC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$B6BE9507-3871-41EF-870B-AB2B548BD75C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$E903B19B-A7E9-462F-A548-50F3030CB443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5710cd0fb8b5907d40eeada6e14d4018e26669a5","datavalue":{"value":{"entity-type":"item","numeric-id":1255942,"id":"Q1255942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$D97DFA58-B7F9-4BD2-86E0-BB355C34EE08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0e3a179147832b2b1c96869b8d44ccac54dac91","datavalue":{"value":{"entity-type":"item","numeric-id":4343990,"id":"Q4343990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$B6E4C5C6-66ED-4A1F-BE64-5B1827CA7BD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cdc7283fe176cc7266c2ab2cb14158c061aab4a","datavalue":{"value":{"entity-type":"item","numeric-id":3613414,"id":"Q3613414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$7B58168E-7EAB-4829-AD59-A158D3019EB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f6d658032331dfb0270d5e1966446426f3c01f","datavalue":{"value":{"entity-type":"item","numeric-id":5326280,"id":"Q5326280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$992CD3E4-2342-4107-BBE6-7731E35F097F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39bb4717d37ef69a929a6409422f87d83adbe2cf","datavalue":{"value":{"entity-type":"item","numeric-id":3638994,"id":"Q3638994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$77BF931D-D397-4E30-A661-32CFDA15909D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8951bab5b7cc87afc21ab97f2c529ca77a26034","datavalue":{"value":{"entity-type":"item","numeric-id":2802468,"id":"Q2802468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156936$02C68A18-B9B7-45E6-A083-054717CC2DE2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"91625fcb25720c84a23c2914149f303ec03f7807","datavalue":{"value":"10.1016/J.JLAMP.2023.100871","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156936$5E6E7268-1AB6-4E25-B37B-8A2BCEA6E3C6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a84e644170331a6a9485b207c047e686cd4d5525","datavalue":{"value":{"entity-type":"item","numeric-id":3826528,"id":"Q3826528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c4f7f13741824543b9231a42c1ed20bd36859bb","datavalue":{"value":{"amount":"+0.86836004","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":"Q6156936$B227EDE5-570E-435E-B6AA-84F5A830B412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ca0bcb65b5468bbb13bd98ff48bab2b186bc3f0","datavalue":{"value":{"entity-type":"item","numeric-id":2703694,"id":"Q2703694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43676cb2d368658f42148152b6467342d77770de","datavalue":{"value":{"amount":"+0.85568285","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":"Q6156936$F52EEF34-FCC7-4A88-91A5-388A88D888AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983cd21deef8e8804b56013c2e7cdcc132ea1307","datavalue":{"value":{"entity-type":"item","numeric-id":2722043,"id":"Q2722043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"939d3e2b467ffb6c0974eda16f5568132699a517","datavalue":{"value":{"amount":"+0.85036474","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":"Q6156936$FBD2F277-886A-4CC8-80AB-98598F58AFB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c15b367ae67621962a2dd23d164a19c1765a25bb","datavalue":{"value":{"entity-type":"item","numeric-id":4023471,"id":"Q4023471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c195118cdbd99ae4d2dfb831b916065237a9b98e","datavalue":{"value":{"amount":"+0.84880304","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":"Q6156936$EC5C59C6-A4FD-47E0-B5AE-444BBC283903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf843841cb0df9d160e31d2390de843ee9c192be","datavalue":{"value":{"entity-type":"item","numeric-id":3067545,"id":"Q3067545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93b2f4d96ad50f8aeb869ad5fa00ddbb05c68a1c","datavalue":{"value":{"amount":"+0.8425945","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":"Q6156936$3DDB84E7-1122-4380-AE60-47EC23C916E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ab94aeda0c95ed5c4c94b16752c4cc41d273ca1","datavalue":{"value":{"entity-type":"item","numeric-id":5217308,"id":"Q5217308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae7e92922787256f5f25d07648a51b32b1f2668c","datavalue":{"value":{"amount":"+0.8409164","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":"Q6156936$421CF815-04F0-4D5F-93BD-884B3435D7C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7223ea97d0680b121a1433900756e5c525b5f769","datavalue":{"value":{"entity-type":"item","numeric-id":4421867,"id":"Q4421867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc533511949f9efc6f211eb83097ca183ba2df41","datavalue":{"value":{"amount":"+0.83872664","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":"Q6156936$3AC21535-F89A-43F3-BBB3-9E25F476FB90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd2774a3ca196ccddeb23f5a1832890dd92b4783","datavalue":{"value":{"entity-type":"item","numeric-id":4424850,"id":"Q4424850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a297d1060f65df00d70abe580d725b03878cfb7","datavalue":{"value":{"amount":"+0.8375952","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":"Q6156936$3A023044-2A25-4129-9D14-AF7637DB23E4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6156936","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6156936"}}}}}