{"entities":{"Q4640971":{"pageid":6670552,"ns":120,"title":"Item:Q4640971","lastrevid":53094617,"modified":"2026-01-24T05:17:19Z","type":"item","id":"Q4640971","labels":{"en":{"language":"en","value":"Survey of research on program verification via separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6874812"}},"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":"Q4640971$9D007564-2464-455A-BC3A-E6F6C5D3E4C1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"59e193c1186d71fa7aee279b9d539f61712456bc","datavalue":{"value":"1399.68031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$0349B5DC-1A4D-460F-B253-109CA8102175","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6240a0e63014b3ab3cb57b4f37c6b5dce0ed710","datavalue":{"value":{"entity-type":"item","numeric-id":436399,"id":"Q436399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4640971$7B6ABF4D-CA59-4F1C-862F-7512093AF5B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8691d93ddee1b7ba60a716fbb0b3547564ea631f","datavalue":{"value":{"entity-type":"item","numeric-id":4640970,"id":"Q4640970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4640971$9205C042-D843-4E81-A313-1767F8EFE844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f10345ef64d56c3ff4d6cb4b89d7077058be7287","datavalue":{"value":{"entity-type":"item","numeric-id":320075,"id":"Q320075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4640971$B8632461-FEF2-4F4E-8030-F207262DC16F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"889be0f8e7c5593fd9d724762872dd9608a4e49c","datavalue":{"value":{"time":"+2018-05-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4640971$6C40AB6E-2BC9-47E6-B226-5662A09AFBAA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$144E37E9-9318-4533-B661-D97642BBFF32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$D4E379F8-5F70-4FC7-B725-457C5DA7C08F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$8F137DC5-A0E3-4A1A-BFE7-C2C3EDF37BE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$05901E7C-FECB-4EDF-A1E2-1FC3B22BB06E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"df61276fde62601f87cba100c079600b6bd02aee","datavalue":{"value":"6874812","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$16F0EF11-FA5F-42B2-B466-F9CDE5E7F25F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4640971$6559252A-9723-4D95-8BF6-1BBED3F33C48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q4640971$F3A47B33-FA89-436B-ADA9-219D10513825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4640971$93D47BC1-1123-4373-AD45-B97DE8B818E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa365f462f7bd1b9fdf8abaedd14810c00851a5f","datavalue":{"value":"memory safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q4640971$DF190441-46FE-4F2A-88C6-A320D265D687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c96bee06122d04aeb6da34b7f304f77e7196b92","datavalue":{"value":"functional correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q4640971$BDE0913F-70B5-4762-BBAF-AD382C04BC95","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":"Q4640971$BFC20A06-94C8-44C9-91F5-E08D06151730","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"34e8e52b6f0163904bb3b10aba94bfa622f7d6c2","datavalue":{"value":"10.13328/J.CNKI.JOS.005272","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4640971$8C9FFB87-8667-4076-B1DD-2A53C17B29EC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc0a6160766d56fcc5b54b16a1441c7012255209","datavalue":{"value":{"entity-type":"item","numeric-id":5883571,"id":"Q5883571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89d7bbe6be3e38fba8714c6d54043a6e5e0c46e6","datavalue":{"value":{"amount":"+0.809714674949646","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":"Q4640971$2D5A7FE9-4FCB-48F7-8011-05503918D06F","rank":"normal"},{"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":"59971d482fdbf8b251b59e2d031e65e472748213","datavalue":{"value":{"amount":"+0.7935022115707397","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":"Q4640971$CA3BC351-40BB-4631-88A7-24C71B696423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c0e0a1f2fedeb51ee6d89ec7c7a7e287388dbbc","datavalue":{"value":{"entity-type":"item","numeric-id":2937786,"id":"Q2937786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c2a04546ecc18828fd9ba7112c0eda7f64a9c2f","datavalue":{"value":{"amount":"+0.7628582715988159","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":"Q4640971$D3DC05ED-2AE3-4D45-85C6-DECA41592305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea93506793d7ae3e9f100eda6c9ed8d96448d9b1","datavalue":{"value":{"entity-type":"item","numeric-id":436400,"id":"Q436400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d71bafca99173cef6e843817f55d3e85726fb839","datavalue":{"value":{"amount":"+0.7625042200088501","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":"Q4640971$E3A014E8-66FA-4C12-94AD-3600FF7C5960","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba2dd604750052f6347b1d760a77fa2c990e8d03","datavalue":{"value":{"entity-type":"item","numeric-id":5452612,"id":"Q5452612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8470fdfb295ac6f7c047dfb1c557dba50fac5d1e","datavalue":{"value":{"amount":"+0.7592105269432068","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":"Q4640971$EC09D866-3CBD-4B1D-B419-411B1C532780","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4640971","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4640971"}}}}}