{"entities":{"Q6550601":{"pageid":14161755,"ns":120,"title":"Item:Q6550601","lastrevid":95548814,"modified":"2026-06-05T09:15:35Z","type":"item","id":"Q6550601","labels":{"en":{"language":"en","value":"Verified scalable parallel computing with Why3"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7860307"}},"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":"Q6550601$2CAA44A5-61A7-4F99-86EF-03D1BFAAD9D4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cb085a3c11181984c696bfcabf2e860e8446c8c0","datavalue":{"value":{"text":"Verified scalable parallel computing with Why3","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6550601$9576664F-93E9-478E-8CC3-06D7622F3FF1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"779efe8d54a9217ff154083930eb748907647f11","datavalue":{"value":"10.1007/978-3-031-47115-5_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6550601$DBC028DC-1870-4A5E-9324-28CE524CE5FA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"df931395300cf18d42380ba7e77d8470c5fc3da4","datavalue":{"value":{"entity-type":"item","numeric-id":6550600,"id":"Q6550600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6550601$CE6A41F3-A782-479F-B18A-CBEF16D5068C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"41523071f7928e35d0476c616da8429088b7716c","datavalue":{"value":{"entity-type":"item","numeric-id":1566917,"id":"Q1566917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6550601$B0EF86BD-A0AC-43ED-AB0A-9C26F6982B05","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5219263c6fa56721869b7c73877f4b0a69654303","datavalue":{"value":{"time":"+2024-06-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":"Q6550601$062ACDFC-9D96-4EDB-8CB0-302F7BD3F07F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6550601$1EE1CE73-D1E7-41B3-9796-D8405AF6140A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6550601$7DB462BE-0DDA-4BD4-8AEA-1D68E92B4AB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6550601$18A31DD1-1AC5-43A0-A48D-3FC681F87339","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1f1dedc2f788d797fa6ba002ee2521363990f1f7","datavalue":{"value":"7860307","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6550601$D1A39856-F693-464D-984C-EBBC74A321CB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"730cc458ac11c87583f4a0fe49183073cd796b92","datavalue":{"value":"scalable parallel computing","type":"string"},"datatype":"string"},"type":"statement","id":"Q6550601$14F06B29-D9E5-4EEB-841C-D6B3E79B9CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00b76a2e54f8798fe172effecd557ced03e2f904","datavalue":{"value":"functional programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q6550601$E9EAAA6D-CD59-46DB-A5E3-64B861508A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaa74f946f4a7cf49359214ccbeddb232ccd2dee","datavalue":{"value":"deductive verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6550601$3A7EEF37-4A17-4186-898E-D062698E9C3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6550601$CF7905F2-FF7D-4457-9592-F6712E923C37","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":"Q6550601$7C95764B-4B90-4F86-9DA2-F8207E36D43A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef4b0f069766f833fa9e7f26c4ddeb447f9ba38b","datavalue":{"value":{"entity-type":"item","numeric-id":3993075,"id":"Q3993075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6550601$267404DD-D28F-4DD2-BD02-25F57F4637B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a92268296e06f7796f62c8fa86f49ced2fef9758","datavalue":{"value":{"entity-type":"item","numeric-id":2011201,"id":"Q2011201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6550601$01352605-4F78-4FA1-9E6E-0963BD23B746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5ca3ee07c04b45f49ba004d5e79bfa76a5be652","datavalue":{"value":{"entity-type":"item","numeric-id":2879257,"id":"Q2879257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6550601$EDD3086D-0814-4F0B-82EF-1D918DB8CE06","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b4eb8bbf73b5e78bf9d7020ee95dee91b165370","datavalue":{"value":{"entity-type":"item","numeric-id":4817290,"id":"Q4817290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"653292e1fec419df1f7a2dfc4bdb3f3bda8cc122","datavalue":{"value":{"amount":"+0.7548850774765015","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":"Q6550601$9F2B0CD5-77B6-464B-9C9B-C7F025A41021","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be316a76491e1d7fc11950ab27bfcc624d436e3e","datavalue":{"value":{"entity-type":"item","numeric-id":4434708,"id":"Q4434708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a25149ba2b146df2bfc11a359186a944e0b76c02","datavalue":{"value":{"amount":"+0.7483758926391602","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":"Q6550601$DCB3C34B-E53F-4F6A-9729-462B671708A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6117039f313cc36a6b6a5200a3ac88da879bcab1","datavalue":{"value":{"entity-type":"item","numeric-id":1566918,"id":"Q1566918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d56f3b9f43d4cea1737d096ce0abed89272ddda1","datavalue":{"value":{"amount":"+0.7333102822303772","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":"Q6550601$98C8C30E-3C4A-4D51-9153-F7C1EC1A4AC4","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":"43b8baffc8e9d7cf658b4b4d53b5d4871a79e091","datavalue":{"value":{"amount":"+0.7049599289894104","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":"Q6550601$59660681-9391-4AE0-999B-A080B9F8A09C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1b40e281eb27f4d8b2c8ba45cf4ec7557ea8be7","datavalue":{"value":{"entity-type":"item","numeric-id":2011205,"id":"Q2011205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2707da559e065741bfb0048c9483a19bf5d9131c","datavalue":{"value":{"amount":"+0.7041804790496826","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":"Q6550601$095109B1-02F3-42E5-A084-17B3D88F7D76","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verified scalable parallel computing with Why3","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verified_scalable_parallel_computing_with_Why3"}}}}}