{"entities":{"Q5739977":{"pageid":7769529,"ns":120,"title":"Item:Q5739977","lastrevid":52572320,"modified":"2026-01-23T00:18:31Z","type":"item","id":"Q5739977","labels":{"en":{"language":"en","value":"Proof automation for functional correctness in separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6601623"}},"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":"Q5739977$529FF5EC-D747-43F5-8354-807016E120BD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f8327f545c2ac3a89fd214f93f99000ace65d460","datavalue":{"value":{"text":"Proof automation for functional correctness in separation logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5739977$8E3C0428-B3BA-4F4C-BDDE-99439EC882AD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ba6d3c362298a0c8079162d1e0d5247d635817b7","datavalue":{"value":"1344.68209","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$818F29E5-1014-4042-8C13-7DB5237C524C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"39eefdf43007a5db029de99b1444c96ff88fcb4b","datavalue":{"value":{"entity-type":"item","numeric-id":667525,"id":"Q667525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$EC3A43CC-487B-4328-AE02-E0D3DB546EFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"982d9eb1fc0eb5fc17fd1d5b1b0dc7d42b2233e1","datavalue":{"value":{"entity-type":"item","numeric-id":685547,"id":"Q685547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$C73B26B2-F89C-42B1-B4F5-1E944866E071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51b90353512d814f6655789de8fa8f4adf362ca9","datavalue":{"value":{"entity-type":"item","numeric-id":656857,"id":"Q656857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$2C72CAA0-5A9B-4B0A-B59E-88E6D79F482B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"83a193227d6ba6906cd45e4bab84652b56c48091","datavalue":{"value":{"time":"+2016-07-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":"Q5739977$920078F6-8404-4D96-A1E0-912A40EDAAB9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"846fa92933f276319aae6b7adcb0db85f6a387af","datavalue":{"value":"https://www.pure.ed.ac.uk/ws/files/20001869/jlc.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5739977$9BA31CCC-3DC6-4913-B89B-21233F1268B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$5EA631F3-5B48-4CB8-84C1-895C37781214","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$CEB0F9FA-A8FF-494E-9671-F91EED623E75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$A25D4C7F-E4D7-4905-8E42-7CF43692895A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$282DC938-766E-4344-ADBF-7F4466E99790","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8070c4f2073988450bce1fca0fc7962a39e51abd","datavalue":{"value":"6601623","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$003AA7AB-F027-4E20-B575-8B4BB79C3872","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e925d21691ae524cbfb2c7846fe00986c22417c","datavalue":{"value":"proof planning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$20E5461A-D761-480E-A25D-26E06FBC67F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c96bee06122d04aeb6da34b7f304f77e7196b92","datavalue":{"value":"functional correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$3CC8F0BA-AB70-4F62-BE8B-FF8FB35804D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"be5b38b87985761f424d5273bb98c8a8d13b7935","datavalue":{"value":"invariant discovery","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$98EB4F02-7849-4D0C-BF55-DAEE5CF1E9E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$2AC792EE-C392-4A9D-8764-E4DF92F96248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e19a56a35da34eb08b4ac43272212a5013c8d21","datavalue":{"value":"substructural logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$5076FAD4-77A6-4260-961A-606EB2F47AE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739977$7D03169E-4FC0-493F-B567-ADF885D20DF0","rank":"normal"}],"P1463":[{"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":"Q5739977$07A7DED6-807A-4330-A672-FD2C0D67D92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab1ccc8faeab7e6c417af9846c477f0e521ebe1b","datavalue":{"value":{"entity-type":"item","numeric-id":14592,"id":"Q14592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$A9DF62B6-AB64-49FF-AC67-FF668D68F902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"493c4272f3e5f72c11a4ab08cd3c037673ba4268","datavalue":{"value":{"entity-type":"item","numeric-id":21766,"id":"Q21766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$ADAAD2B7-C023-44FC-9B46-D77445FFCCD8","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":"Q5739977$F8E2DD47-1607-4F97-B96D-C42DE5ED2D73","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"93f0ffb1d5817013d97a3de81dd0d404e8ffdc79","datavalue":{"value":"W2325932479","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$BF3DFF18-07ED-49C2-AACA-5667EAE02DA8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7f23884f9b9c6a13956150c218308489799f0e84","datavalue":{"value":"10.1093/LOGCOM/EXU032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739977$CE9A9FA5-9A67-4C8F-82DD-A43980594C1C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739977$0B682405-9A53-4DF9-8BD8-1542BD3C99D3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"653bb42b19be8ce2e8f831ce06cf512b9e69994f","datavalue":{"value":{"entity-type":"item","numeric-id":5311261,"id":"Q5311261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d8ccd2029022d2d2833e8d3969047b785a9f1c5","datavalue":{"value":{"amount":"+0.7745450139045715","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":"Q5739977$924500CD-87B4-45C6-9E53-23A4BC1D5043","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d92a25c4769b60bedd453035abfc39902034de3","datavalue":{"value":{"entity-type":"item","numeric-id":3460548,"id":"Q3460548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ee21699dc1ecdb8610323b159adc13692478835","datavalue":{"value":{"amount":"+0.7633259892463684","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":"Q5739977$B1863383-C5A0-4AC8-AE88-B772AD18575B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ce9665b91ecb3a2eb7e60be16e012a2320e66e4","datavalue":{"value":{"entity-type":"item","numeric-id":5200020,"id":"Q5200020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7e0f6c280548524b7d51250cfe97a66db7e1a60","datavalue":{"value":{"amount":"+0.7616608738899231","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":"Q5739977$949A16DC-8408-42F5-9A20-C2D09F5278C9","rank":"normal"},{"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":"4c06384c6bdc0f5a884812f79bfc3efe0ae60e46","datavalue":{"value":{"amount":"+0.7614348530769348","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":"Q5739977$624AF60B-CF2F-4F30-9873-B59F3337E499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59554135aeae70a26490f68ca0b06ddbc8ea8090","datavalue":{"value":{"entity-type":"item","numeric-id":5493374,"id":"Q5493374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"502298a541db50c4b4413b631578f9b172f72433","datavalue":{"value":{"amount":"+0.7542544603347778","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":"Q5739977$2AA3D592-5765-4449-BC94-33A9FDDFAED3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5739977","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5739977"}}}}}