{"entities":{"Q6113015":{"pageid":13247322,"ns":120,"title":"Item:Q6113015","lastrevid":57443082,"modified":"2026-03-30T23:13:27Z","type":"item","id":"Q6113015","labels":{"en":{"language":"en","value":"Verification of mutable linear data structures and iterator-based algorithms in Dafny"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7723896"}},"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":"Q6113015$75478A8C-619A-4627-9E76-24812E5B19B9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"efe3d1838e3204dfce4baa1948ccea5a22cb9bee","datavalue":{"value":{"text":"Verification of mutable linear data structures and iterator-based algorithms in Dafny","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6113015$8B41F754-6B9A-4E00-94ED-84B22B64E632","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"abfe16028ff32a4685b8bfff56a67d236407f60a","datavalue":{"value":{"entity-type":"item","numeric-id":6113014,"id":"Q6113014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$B4DCBFAC-1318-48FA-98F1-362EB4475596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc554f6471ff9eed49aa19334a728f6412a548e6","datavalue":{"value":{"entity-type":"item","numeric-id":209390,"id":"Q209390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$043CDC75-2B59-46C3-8A5E-F350669A4425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a7fe0d5d94c9e0413608077b92ea1c7fc83d2414","datavalue":{"value":{"entity-type":"item","numeric-id":2437793,"id":"Q2437793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$A0E1EC2D-1E11-40B0-96BF-8358CE2605EA","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":"Q6113015$311E3486-D411-4421-ADA0-890294E37EFD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"38bb85a5ba91301ec8d8e3fe04a5ca58f334ca78","datavalue":{"value":{"time":"+2023-08-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6113015$F3B11D88-C6E1-49C3-A7C3-E57F353BE29D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6113015$9D3D2A87-AD22-4A46-B02C-64C39E1253C0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4b6cff6892e14caac7a1854630b6c4f69edc1c1d","datavalue":{"value":"7723896","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6113015$EE4F2CED-052B-44ED-9282-B076E677533C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6113015$0C569991-72A6-4C29-B2EB-2695CB84B1BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43d8de44b3f88bd19a871628a3509981cd748562","datavalue":{"value":"data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q6113015$C98A97C7-743A-4289-BC0A-9D810316A87C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e1daee68cedeeadccdf496f924561e3065e4444","datavalue":{"value":"abstract data types","type":"string"},"datatype":"string"},"type":"statement","id":"Q6113015$4215C751-BF81-454B-A61D-780EB2B69680","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c50f6f299b28ee61b1675f63af1267482fef0a6","datavalue":{"value":"iterators","type":"string"},"datatype":"string"},"type":"statement","id":"Q6113015$4747EC60-8894-48B0-809C-460FA9DD22A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8bc3fcda11d6808794c792f39897873e5d3efa3","datavalue":{"value":"Dafny","type":"string"},"datatype":"string"},"type":"statement","id":"Q6113015$183A69C4-65F5-4EDC-BF70-52B0F66DD6D9","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":"Q6113015$3E020C26-E753-4923-A152-8975F4AD8C72","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$20E20A46-F090-4B67-B694-CA5E475A2CA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e044e9e3b21b228718f89e1b64de2c48e2e3f3d","datavalue":{"value":{"entity-type":"item","numeric-id":2875082,"id":"Q2875082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$B667E2DC-72A3-44F9-92DF-5D1EDCB73071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2783b262b45229c044817d7b28465fa7e095f5ab","datavalue":{"value":{"entity-type":"item","numeric-id":3012966,"id":"Q3012966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$60A39449-2638-4B32-99A7-9E12362D5542","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dff1404f0e725829a18605baf0b0312d0d24d638","datavalue":{"value":{"entity-type":"item","numeric-id":6113015,"id":"Q6113015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$BFAD0E4E-20D4-411F-A1C6-BEE4AF2E7B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ceeca403a06d4d6cd0a3d454da656e6f4d93aba","datavalue":{"value":{"entity-type":"item","numeric-id":5899012,"id":"Q5899012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$9A879346-9562-4D71-92BB-65FF2612B0CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4cf01f6d0f15e194b18b50e7192ec30c2fbfafa5","datavalue":{"value":{"entity-type":"item","numeric-id":2507783,"id":"Q2507783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$AF7C2AFB-E0A6-4C90-876A-90AF7B8250C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"732f0c69558b483d8455a94e6c32f777993f0182","datavalue":{"value":{"entity-type":"item","numeric-id":4855425,"id":"Q4855425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$4A61B3A9-D677-4E88-8C72-91819B0BACE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d635bdaac719356d8a6cff12d936845108210d2","datavalue":{"value":{"entity-type":"item","numeric-id":5756488,"id":"Q5756488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$6A173502-AB7F-4432-9DF5-8004B155857F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4709bc1ae6aae66f69f3beda3cb2cfdb6046e366","datavalue":{"value":{"entity-type":"item","numeric-id":2512398,"id":"Q2512398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$2FFD588D-2BEE-44D7-B8C8-72F7D4A6CEE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"734731b9d85ca7dc3b484125f379ebf0f21401ef","datavalue":{"value":{"entity-type":"item","numeric-id":3585053,"id":"Q3585053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$2D638843-0FDF-4423-AD47-0A3227C5A5B8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"83e40d1102c586fe5b2acde7a017da2d1cfd7d2d","datavalue":{"value":"10.1016/J.JLAMP.2023.100875","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6113015$D2F40CD8-7552-4493-84AF-2F0E5CC95DC3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4018c02e7db9904c539f4028ab9c71426b90cda2","datavalue":{"value":{"entity-type":"item","numeric-id":2467973,"id":"Q2467973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef0ee7cab93fd3b37e0c5f6f0f22ad9943963ea3","datavalue":{"value":{"amount":"+0.88127047","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":"Q6113015$9810D998-63E2-409E-8432-0D91365749F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"406bfd2ba0200296a70457b3b3c22f7123ba776b","datavalue":{"value":{"entity-type":"item","numeric-id":1974308,"id":"Q1974308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cda8dcaf871ab9c02d1142cda5c45687dfffc3d","datavalue":{"value":{"amount":"+0.8790078","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":"Q6113015$77C7DAAF-2994-4AA0-B3D5-802E3BA4D9EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3fbb8e3c6b78474ad8791668e2afbe6fc2876e1","datavalue":{"value":{"entity-type":"item","numeric-id":1403234,"id":"Q1403234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"184db956127ed7b88492690f98a8ffca797f9b91","datavalue":{"value":{"amount":"+0.869889","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":"Q6113015$6E768545-27D3-41E9-A740-60CC65E974ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"454edc56852e5e8c21d65e7220104fce812e9362","datavalue":{"value":{"entity-type":"item","numeric-id":4517376,"id":"Q4517376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9027f51d8c92fc34fa2dcd36263737fcafa9421c","datavalue":{"value":{"amount":"+0.868106","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":"Q6113015$371F5515-BC3C-4319-83A6-5731026C831E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3988132bf5a8fe91a1c53f6f9a823d6cd6b35907","datavalue":{"value":{"entity-type":"item","numeric-id":1664147,"id":"Q1664147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"084479341feb7471455bdcf6bbcf8a61c72e6ae0","datavalue":{"value":{"amount":"+0.86808467","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":"Q6113015$8AF0A6B2-61BB-432E-AFC0-C93629C63041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"babed51588151eca4da090d9aa82a91f54a056d7","datavalue":{"value":{"entity-type":"item","numeric-id":2863858,"id":"Q2863858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10b0043465fec1016863f7c0621cda6455f3f008","datavalue":{"value":{"amount":"+0.8631309","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":"Q6113015$85E0A235-145A-4D31-9AAC-90B6EAD94955","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12f99f5038c2994757504732f87e7e7cf296885a","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b76ef0208e29bcd837eda26e4a0f758599821406","datavalue":{"value":{"amount":"+0.85658944","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":"Q6113015$2586C91A-BE30-427F-9EF5-52D98D2C7771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e3490f34d0d6ba2f54fad3208ae926689909c6f","datavalue":{"value":{"entity-type":"item","numeric-id":1664150,"id":"Q1664150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd0f2f80978fb57672f3b2937ceaa0bb45f81c89","datavalue":{"value":{"amount":"+0.85410833","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":"Q6113015$AF06CCC0-C2EE-4AEA-ABC3-94AB8951C6A0","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"c39a117a349789e54237c0a3254f5a10c0a6517e","datavalue":{"value":{"entity-type":"item","numeric-id":6830565,"id":"Q6830565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6113015$54C1811B-2F2E-40E2-856F-DF6C556A1CB1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6113015","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6113015"}}}}}