{"entities":{"Q3066108":{"pageid":3076824,"ns":120,"title":"Item:Q3066108","lastrevid":51159926,"modified":"2026-01-17T00:09:45Z","type":"item","id":"Q3066108","labels":{"en":{"language":"en","value":"Dafny: an automatic program verifier for functional correctness"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5834048"}},"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":"Q3066108$8FE31399-1CF5-4C8A-94E4-ECB76139F77B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd27ed19d6c8054c2a219300722141b6f6758700","datavalue":{"value":{"text":"Dafny: An Automatic Program Verifier for Functional Correctness","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3066108$6FF6EDB2-698A-4C8E-B0F5-C1213F1B5129","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"040ae9a283f85c362ffe665a93469af82efbbd25","datavalue":{"value":"1253.68095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$3DCB8524-5FEE-4307-A7EB-7163B91802C5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e2020442925256b51bce848f128ac7752fa0df9e","datavalue":{"value":"10.1007/978-3-642-17511-4_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$D8425877-418B-4E52-9A11-CD67A819A118","rank":"normal"}],"P16":[{"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":"Q3066108$4B5183BE-5C02-4813-AE02-26ED3D480227","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$ADB92A24-37AF-4530-A1EF-16901CD8862E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"156b753d324324fc03cf856ff2e3142887c3187a","datavalue":{"value":{"time":"+2011-01-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3066108$7AAF9BCF-2000-44AE-AC50-95473802D060","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$3C9155E6-38E0-4743-936C-3E3E1A6FE26C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$28BB39BF-BCEF-4489-B2D2-0091C474F7E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fecffe08e42df4db62551619227b8cf34f075863","datavalue":{"value":"5834048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$F03B3271-492E-458B-AA9A-CEAD8CA04EB4","rank":"normal"}],"P1463":[{"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":"Q3066108$6088DF9D-034B-452B-91B9-B66CD35E650C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"beb205139d0971fca32ffa61e5b55aaac31a7181","datavalue":{"value":{"entity-type":"item","numeric-id":16768,"id":"Q16768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$A6B46EAD-6EB0-441F-B155-807C0B825CC1","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":"Q3066108$FACBB736-831E-49FF-A8F7-4395A7291BE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d618f2518558acd5a4de20ebf1f4d24983053a90","datavalue":{"value":{"entity-type":"item","numeric-id":21728,"id":"Q21728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$1F86CBDC-7AB5-4562-B3E6-63D5D6B081F2","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":"Q3066108$B4961C0B-DCC9-4AC1-A7C8-03D8805770D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$E2E007F4-DB31-487B-A3CF-41EE55B838FB","rank":"normal"},{"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":"Q3066108$81C5E50C-2689-4E66-B593-D51370D2283D","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":"Q3066108$B2B26E8A-1EFC-4625-80F1-D095F609B64E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb4ac1b3e6590933f07db2ef44e8e77f8844e4b4","datavalue":{"value":{"entity-type":"item","numeric-id":19271,"id":"Q19271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$EC1A43D2-7B8F-47D6-BB39-F792546CB2D9","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":"Q3066108$62179D1C-2EB4-4387-9A8C-FE2970224C1A","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":"Q3066108$BFD1C785-998B-4DF8-9F3D-E9438DA0B5C8","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":"Q3066108$4EE36277-BE10-40B0-BAF3-3E2ADBAF6593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1637c3ce3f61a15997b947ec05e883d55623946c","datavalue":{"value":{"entity-type":"item","numeric-id":19722,"id":"Q19722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3066108$D3D59165-10B0-4ED7-B7E4-460EFB295F9A","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":"Q3066108$17580D28-9CC3-48F0-8731-BE82A6D6811D","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":"Q3066108$43725B0E-A057-4ADC-8EEB-542CFD0A03B8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c8a2d5a20b4a777cac0326519e8f4721b168db38","datavalue":{"value":"https://doi.org/10.1007/978-3-642-17511-4_20","type":"string"},"datatype":"url"},"type":"statement","id":"Q3066108$4A654459-986E-4660-9F12-BDBF1AE89C32","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b5e8be416d574afd56dec18dbee52f286c2b0bfa","datavalue":{"value":"W2130427425","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3066108$C99F1434-C39C-4A85-A8C1-C557F71E9EA3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9babaf2bd52e8d0585eb0dfafb2c1d459313c380","datavalue":{"value":{"entity-type":"item","numeric-id":2908486,"id":"Q2908486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbabf198357237051f5d48f27c94952aa0fc2adc","datavalue":{"value":{"amount":"+0.7574963569641113","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":"Q3066108$FBACAE3D-0B38-41AF-9408-A6210F8FA3A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e4f7550369b8e1b947e819d750997574708bd86","datavalue":{"value":{"entity-type":"item","numeric-id":5900714,"id":"Q5900714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d48b78c754d62c9163efae0f356d26fb7776946","datavalue":{"value":{"amount":"+0.7542292475700378","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":"Q3066108$707AFAA7-609B-413B-A6D3-56E84E10FB42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf00a775bd635b9535e48b7dcfc8aea2cc944962","datavalue":{"value":{"entity-type":"item","numeric-id":3196351,"id":"Q3196351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46f4a912fead79ceb086464e14ae18012983a58f","datavalue":{"value":{"amount":"+0.7541444301605225","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":"Q3066108$04198E21-C79D-4D28-825B-EA1EAC6069D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d368107344918cf344e91551289f3ea49aa9f173","datavalue":{"value":{"entity-type":"item","numeric-id":3189836,"id":"Q3189836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"761d9db23aca0756069ab433bb622be00ea73f05","datavalue":{"value":{"amount":"+0.7540255188941956","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":"Q3066108$7324931F-A815-4AA3-8AB6-9CC04B4D79DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"82d170e51fc2e631d9cc31c3155e279e1d9e0a46","datavalue":{"value":{"entity-type":"item","numeric-id":5739977,"id":"Q5739977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc68358f71b59bd883e11431f7b316ebd64edc00","datavalue":{"value":{"amount":"+0.7539809346199036","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":"Q3066108$7C27F940-579C-4638-84D9-E7112FA59244","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3066108","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3066108"}}}}}