{"entities":{"Q2324204":{"pageid":2334947,"ns":120,"title":"Item:Q2324204","lastrevid":71844414,"modified":"2026-04-14T00:55:03Z","type":"item","id":"Q2324204","labels":{"en":{"language":"en","value":"Efficient verification of imperative programs using auto2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7105310"}},"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":"Q2324204$53A60F9F-3BC5-439E-A8FC-BFCF6235C029","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a884c852380a260760331ebe4ca303e864ce11c9","datavalue":{"value":{"text":"Efficient verification of imperative programs using auto2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2324204$E6C7D883-E953-4DA4-83AA-86C479A3BF4B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1b019fa6b891ba6824e74679da83dd02805fdbed","datavalue":{"value":"1423.68295","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$3CDF5C3B-0B9A-4649-9694-7C98330C6B27","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bcd3412dc85d29d8fd65af240941af23528afaf5","datavalue":{"value":"10.1007/978-3-319-89960-2_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$A09EB44A-7204-466D-A6D1-6FB930624727","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d47a0b532fadc119a2da0b4f59e3906ea7d12d94","datavalue":{"value":{"entity-type":"item","numeric-id":258840,"id":"Q258840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$2387A07E-844E-4C58-B793-51ECBF65FB6C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96391af82153a94a4af2a0e4c8ac60042cea1674","datavalue":{"value":{"time":"+2019-09-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2324204$769BFCA1-FDC4-45C4-925A-4E800E17873F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1d58738d6f6b46813cdbef81f835ce0468bf36e4","datavalue":{"value":"https://arxiv.org/abs/1610.06996","type":"string"},"datatype":"url"},"type":"statement","id":"Q2324204$B07B8E36-23E1-4509-B57C-7F63C5FE1BE8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$E8947F5C-4DC4-4EB3-BE79-14790EDBE0C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$419FCE71-3F3E-465D-AA3A-45C3FA19282A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$0861777C-46B7-4E86-B543-D3BBD176BC14","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eab114a7d2e0141c387da43a0a561b98e84f9493","datavalue":{"value":"7105310","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$6AD14FB5-46E1-462B-8364-F00B3030E37C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$02A0C843-2E1B-4256-BB8E-44ED796C7014","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":"Q2324204$B29E7CE5-93DA-4047-850E-6C72445903B2","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":"Q2324204$6B4ADC53-3C60-437C-8E91-31BB5070DEC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f86a777ed9723a1505ce676eeb86cd88f8987a7e","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$3FEFC9E7-4317-4508-8EFC-D0775D04AFF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d082feafa45d8fd2af5638ac3cc0080de90d3ac","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$3E25D57C-DD57-4253-B4D6-C979887860BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$6784AD14-D10B-4AD0-85FC-27FA1AF41F78","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":"Q2324204$4BFB2CB7-BA49-4D3F-B50E-4FB24ECED68C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"665b81d9c0f077e3e09c3e4e80080780b437ea70","datavalue":{"value":{"entity-type":"item","numeric-id":40264,"id":"Q40264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$8841E1C9-9836-44CB-B01F-82F29D4FEF9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e7faabf74dc18d0f41bd3f5c99c24fed967b6378","datavalue":{"value":{"entity-type":"item","numeric-id":29452,"id":"Q29452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2324204$467441AF-4462-4A69-8571-635C505424BC","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":"Q2324204$E0630A5E-DFF9-4AE3-808A-FBF223371C65","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6aed54177ac1b20e0dacbb5911522cca4cc4f48b","datavalue":{"value":"W2765411061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2324204$040E6363-9A6D-4005-9209-62686B406153","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"075a66c739a652c02941396b90f65f06b793f2ff","datavalue":{"value":{"entity-type":"item","numeric-id":3055745,"id":"Q3055745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bde6ebe327708ed4ff6f569ccfcd86a6160e5b45","datavalue":{"value":{"amount":"+0.8879606","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$0336A9B5-BB0C-49FD-AC98-38012CB12FE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1f6a58fda84ce2b1ec77c3acde53b995716dc14","datavalue":{"value":{"entity-type":"item","numeric-id":2931785,"id":"Q2931785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd4fb19459a7178ce3777f2a238cdcdaeb318a6e","datavalue":{"value":{"amount":"+0.8867001","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$2A6EA13B-7D11-4523-83E9-D0403D47F797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5547e7f140f28686cbd763d65679684df419834d","datavalue":{"value":{"entity-type":"item","numeric-id":4551152,"id":"Q4551152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f8ea79e729f7fc15cd7327aed37208ee64a72d6","datavalue":{"value":{"amount":"+0.8806186","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$802401C5-81DE-4122-A491-816EEBC1DA0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4952467c9336251bae4d26323a37a14d83e57d90","datavalue":{"value":{"entity-type":"item","numeric-id":5699474,"id":"Q5699474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61375e917ed215483a97db8d1be11b6b4a74a4c9","datavalue":{"value":{"amount":"+0.8801733","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$A52FF669-ADAC-4D1A-A117-DC258A140E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c36bb3b7997cdc30ca485d27ddbe8d0815f80c3f","datavalue":{"value":{"entity-type":"item","numeric-id":2979818,"id":"Q2979818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbf3ca9ca76d0c475f7ddee3d9bcbf24485c3d08","datavalue":{"value":{"amount":"+0.87918335","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$AF23379F-DEB5-45EA-9295-000CD26AFEC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfd98f2abb2e6d695d1a88d96506627a8bad2bbf","datavalue":{"value":{"entity-type":"item","numeric-id":3575262,"id":"Q3575262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2dd40eb60db6d092df4a36442bd53cba7aad1515","datavalue":{"value":{"amount":"+0.87741995","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$D8581B9D-01C7-4BAF-9A69-DD50C4826D1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5ff7130f3d41e7165dba4d7b35aea65f278b22d","datavalue":{"value":{"entity-type":"item","numeric-id":4700385,"id":"Q4700385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a599f46bf8e9ad9979ab9097a9a7e0c2c0ecb4f3","datavalue":{"value":{"amount":"+0.8753835","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2324204$9258FE9E-235E-4403-9099-A7B2992CF5A9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient verification of imperative programs using auto2","badges":[]}}}}}