{"entities":{"Q43957":{"pageid":44013,"ns":120,"title":"Item:Q43957","lastrevid":105428585,"modified":"2026-10-09T10:10:09Z","type":"item","id":"Q43957","labels":{"en":{"language":"en","value":"Auto2_Imperative_HOL"}},"descriptions":{"en":{"language":"en","value":"AFP entry Auto2_Imperative_HOL"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"e84ee395d70c0619dbd8f3441f4608fff644d78d","datavalue":{"value":"32246","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43957$7B6CF0C8-16B7-4442-A026-4C37EDE40A94","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"8ae17d98a9b6a1d1f81d5f10a4712d1f70997ece","datavalue":{"value":{"entity-type":"item","numeric-id":2324204,"id":"Q2324204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$37FF342A-09B7-4BAE-83C9-24F955CB83CF","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$449A3E71-4039-4987-820B-98F7274EF69A","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"66bce25f4003935a56a806a8800e8a2bdcb2dfc1","datavalue":{"value":"https://www.isa-afp.org/entries/Auto2_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43957$A091A7B3-CD0A-4249-9C89-80EF30FD0057","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43957$199B1CF0-6739-49A0-9010-36BA58CDCDB1","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"845fea984bd3d6706acc856d0595755051e72c0c","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$997CEE33-938B-4A97-B281-E05FBA79D26F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5a90f59e98daa7490325c2b5f9c5a5a63b8942a7","datavalue":{"value":{"entity-type":"item","numeric-id":29452,"id":"Q29452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$39DAE042-BBF7-49D4-A46B-65174895A318","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$46FC967A-D79E-4806-8B5C-DAC363BEB328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$78B8B093-E678-4103-99B0-069FC1590AC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$5CDE6EDC-38C1-4E89-AC95-97470C77E168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e600fcf4c16bf9bbec6afc7a64801eb6824b335c","datavalue":{"value":{"entity-type":"item","numeric-id":40264,"id":"Q40264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$DB35E8F9-2067-44AF-948E-642BAE9D2127","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ccca80b6de24b80a4ce2a4ab4e48d31e9686f36a","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$5ACE44A9-7C29-41B3-8E62-5CD60A90E98B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ce995af0d54f8ab3594278c155d6ae4d6e3a6165","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$DA27267A-EBF1-4461-A740-16042673A475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"750318cfe328b0c4f7914e491e85258c103e5abf","datavalue":{"value":{"entity-type":"item","numeric-id":19722,"id":"Q19722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$41D13F22-B969-4686-BE9D-B169E9A479A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"263af5c0df32ed66fc675fae4932e71337532265","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$270D6FB7-FF1C-4E87-AD4F-E59D4F0592FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"30c6b3cd0def4321e84267e90719462e2335afdf","datavalue":{"value":{"entity-type":"item","numeric-id":39280,"id":"Q39280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$F62D24AB-25C4-4EDF-9B0F-DF1FFEE49ACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7d1a8519018039436924ad678b461ed447b5bd71","datavalue":{"value":{"entity-type":"item","numeric-id":40310,"id":"Q40310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$B8FBAA71-C938-448C-B9DA-2C6624842809","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"97473639ec969c4bd205167b5490e46ab87bd594","datavalue":{"value":{"entity-type":"item","numeric-id":41252,"id":"Q41252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$0E3F5C04-4ED1-4813-B053-6F5D5B757D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"87a0d437bd9fe1eedf9e3f8e0a5bdfc771637764","datavalue":{"value":{"entity-type":"item","numeric-id":41251,"id":"Q41251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$B19430CB-7493-4CFD-A523-2E11605E4F47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7e366e7ad793e17029c92e0a9db53146b13f2367","datavalue":{"value":{"entity-type":"item","numeric-id":34516,"id":"Q34516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$4C514F86-61E4-40E4-B3D1-192D2DD780C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$F6434E32-82F6-4BD9-9062-3990EF1B96E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7ea0a87649edd4cae39bef36b6b305a729532abf","datavalue":{"value":{"entity-type":"item","numeric-id":39832,"id":"Q39832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$8BACE4DC-F762-409E-8846-C81926B3E863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$F5CAFC11-033A-4C07-B71F-CFB3735902B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"07eb0f28b45c8f9b5cf112bbf02e95717fb938ca","datavalue":{"value":{"entity-type":"item","numeric-id":25202,"id":"Q25202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$7B2D6561-F6A8-4149-BD8B-A879FD959572","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a1b5c5e89994fc263bfa438d98cd6199a02c730","datavalue":{"value":"https://isa-afp.org/entries/Auto2_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43957$12E4F625-B76A-4598-A9F3-5CE581131319","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"01aade34926865f306029ac4b82b2852e9efa5b5","datavalue":{"value":"Bohua Zhan","type":"string"},"datatype":"string"},"type":"statement","id":"Q43957$B68A462E-CF9F-40A5-8612-97408B9C526B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d50381b373a1a6e6d6cd6b4293ae09d66615fcd4","datavalue":{"value":"This entry contains the application of auto2 to verifying functional and imperative programs. Algorithms and data structures that are verified include linked lists, binary search trees, red-black trees, interval trees, priority queue, quicksort, union-find, Dijkstra's algorithm, and a sweep-line algorithm for detecting rectangle intersection. The imperative verification is based on Imperative HOL and its separation logic framework. A major goal of this work is to set up automation in order to reduce the length of proof that the user needs to provide, both for verifying functional programs and for working with separation logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q43957$AA99700B-4E8F-41B9-91FA-99739DBDBB65","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9194e9b150f8488fef979658da21ddd0e60751fc","datavalue":{"value":{"entity-type":"item","numeric-id":3651735,"id":"Q3651735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$D314A016-E234-46EB-9E81-13E629D2DBFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$93C6E7D3-BA10-48C4-A505-243006AE3017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"561c39284ec9421bb8483b2aeef47c80a5eebeb1","datavalue":{"value":{"entity-type":"item","numeric-id":2829265,"id":"Q2829265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$F8F8F938-EE2B-4A8D-A056-75B21A8947F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da5b389dccb05fe2dd61d661d50f9146c3a64d94","datavalue":{"value":{"entity-type":"item","numeric-id":2324204,"id":"Q2324204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$9E67F62E-D8E0-4CC9-8DEB-97592F144676","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6b3e8ce19e9f5978e8f566795e3d4c40e60d6b31","datavalue":{"value":{"time":"+2018-12-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q43957$68085BA4-B1E1-4470-A99D-6C0824DD6BFB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d033841a4238fd22e7b61366df380f292e68f0a0","datavalue":{"value":{"text":"Verifying Imperative Programs using Auto2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q43957$0EC518A3-DB2A-464F-808B-DE2DE98F8813","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$92C5AE8D-D04B-4AB7-AE9C-55ACAF52FD8F","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"fc54e444b627294d797222da645a22660a0c742b","datavalue":{"value":{"entity-type":"item","numeric-id":7361272,"id":"Q7361272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$BCFE9C5C-3014-4F0B-810C-77426F607777","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43957$74C6EAB8-F4A5-4877-A21E-111461CA7CF9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Auto2 Imperative HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Auto2_Imperative_HOL"}}}}}