{"entities":{"Q2417849":{"pageid":2428592,"ns":120,"title":"Item:Q2417849","lastrevid":53436698,"modified":"2026-01-24T23:14:55Z","type":"item","id":"Q2417849","labels":{"en":{"language":"en","value":"Completeness and expressiveness of pointer program verification by separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7060928"}},"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":"Q2417849$23AE55F4-0C2F-42BB-B593-BD0C65E57542","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ca33b789144f41a972c62ce5ca4b1d06498baa7e","datavalue":{"value":{"text":"Completeness and expressiveness of pointer program verification by separation logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2417849$B80130B7-4666-4180-B562-B5329EF902B9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"919ccb7d9605d569abf922c4cac53cf84f62640e","datavalue":{"value":"1422.68038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$E5CCAFED-477E-4CDB-B167-7D499DC59F65","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a26d759a8f15177451aa97ef2fc9836978dfb443","datavalue":{"value":{"entity-type":"item","numeric-id":278746,"id":"Q278746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$286F496D-8DC1-4186-96C1-935F0AA2861A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7350aed0b0267db3934820cd5357095f0cb6b7b1","datavalue":{"value":{"entity-type":"item","numeric-id":238508,"id":"Q238508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$70E8DB0D-7359-40EF-9B93-943DB9ABCBDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"831e53c48bbe450043093e4eb2ab3787216fc55d","datavalue":{"value":{"entity-type":"item","numeric-id":278745,"id":"Q278745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$CB56538A-2EDA-4B6B-9483-C23FD9299158","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$6B37BD42-843A-46A5-812A-353E9C3D75EF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6120eae74d684c2ead20d43fdd3e39763954793c","datavalue":{"value":{"time":"+2019-05-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2417849$4DED77FA-9E4A-4086-A2D8-FB2AF1E89CC8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$AED9F291-9623-464C-93BC-0A724FA43C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$BDB3888E-60C4-4E1C-AC71-3F94C59B83F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$E04AD7CC-74F5-48A3-8711-D4B53844A484","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5186d4d63363273c99059915fb8bb7f10e509c91","datavalue":{"value":"7060928","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$E6268EFC-CBBB-4834-9E1C-20C30EAE268C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6ca3089f4a9c1f132e8f874f7fe0c6338d24ce7","datavalue":{"value":"Hoare's logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2417849$36896069-1C30-49CF-A1CE-B57AB46F24FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2417849$6F7E88DF-A6C7-44FE-AF4A-9FD16D46D07A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"669e1ab0be3b0e96a51a2ef7e433c212210f37a0","datavalue":{"value":"completeness theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2417849$1FF485E6-1D62-41CD-B705-D1A860D4A37C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d448dd76afb9a34383e427040cfef5aab7d44504","datavalue":{"value":"expressiveness theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2417849$57F78BB8-DB34-4B0F-A82C-D11F4A7879B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70069efd410315900f2bf16a0133ae36112e66f2","datavalue":{"value":"inductive definitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2417849$F01AE740-2335-4701-B6F1-B9A7E90EEC03","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"101cc42e2ce1fda0eba4e4e50b6e4daaef6c81ea","datavalue":{"value":{"entity-type":"item","numeric-id":21765,"id":"Q21765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$9EFA4C40-D51D-451C-9ACB-6CE201201819","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":"Q2417849$E2EA7F3E-4F07-480D-86CF-1066FAC972A7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c18f1d76a52235e48c2cb2ee2951460d63abfd1d","datavalue":{"value":"https://doi.org/10.1016/j.ic.2019.03.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q2417849$99738656-1146-4EA5-BA1F-5348419C582E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b583159f95bec5f583ee49a1951d7430ac7e21d1","datavalue":{"value":"W2921741905","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$9226B416-2D94-4813-8AC5-BEB8B5A6F2B3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c16a3a901c59b73e252c7c2c8ed885178a406401","datavalue":{"value":{"entity-type":"item","numeric-id":278747,"id":"Q278747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$2CF03E53-A6D5-49B3-B0A4-92A80CE4E74F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$7F73A4BE-157B-4FCB-A835-85C1B466A49D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1da1cf5a701a96be6e2b4fe8962f9ab5cf74c40c","datavalue":{"value":{"entity-type":"item","numeric-id":5493374,"id":"Q5493374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$7385EA6A-577F-4527-99DE-07E792B481D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c23a54cf5c2c32f027cfca2700657a849c9c7aec","datavalue":{"value":{"entity-type":"item","numeric-id":800082,"id":"Q800082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$8612522B-7094-4A82-9D82-1C7790D13759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f9e8e1fe138d59390014af6d7c1a08c93029421","datavalue":{"value":{"entity-type":"item","numeric-id":3611996,"id":"Q3611996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$5D36F27D-EF8E-43C5-B314-30ED886B52C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea8839917919f90fa144382a094d8dea8f58a77f","datavalue":{"value":{"entity-type":"item","numeric-id":3189830,"id":"Q3189830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$E3AD1175-C42E-4328-A476-2BF59C706357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"329632390571b70c858fb813a0e714410ba89992","datavalue":{"value":{"entity-type":"item","numeric-id":5200020,"id":"Q5200020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$289A1FA6-A233-4B89-AD6A-1D742E1F7B7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"110e04d4625ac7707eb0d6fa980c0954dd5abff2","datavalue":{"value":{"entity-type":"item","numeric-id":5705900,"id":"Q5705900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$98A6E44A-1FBF-4482-B405-41C74D15D772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c013e136cb03e4c5ab8c3a7e8c7df1e0a2f62e41","datavalue":{"value":{"entity-type":"item","numeric-id":3189791,"id":"Q3189791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$28C73D24-90C6-4E65-8B30-7ECCB7D45169","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"625d0e546f584fff0965159489d2fe578acb6ad4","datavalue":{"value":{"entity-type":"item","numeric-id":436400,"id":"Q436400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$9F8B11D5-68AB-4F53-8565-03533A2BF592","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$C0EFDE36-8517-4577-A578-BC6D2200B78C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"541bc36e9357802534d1e52134710ec758d76fb7","datavalue":{"value":{"entity-type":"item","numeric-id":5753923,"id":"Q5753923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$0BD66506-B7AB-43CA-874B-A75D7AA302E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66ad83169ed8389564075d9eacd3961be1c6400d","datavalue":{"value":{"entity-type":"item","numeric-id":3189843,"id":"Q3189843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$8559C18E-A691-4640-B50E-79619F803D16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac23d65a9afeff852c7bda4556ad42907e525e44","datavalue":{"value":{"entity-type":"item","numeric-id":5178870,"id":"Q5178870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$2D7D9314-ED49-4316-9749-8A49C172F9E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95e0aa807f915e26300ea89577d46a95b8c17c06","datavalue":{"value":{"entity-type":"item","numeric-id":3334976,"id":"Q3334976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$FB4E9073-BAA0-4EC6-AD5C-C576FA372C51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be22a32095acbcf7e833dd1ccc7a785418185f62","datavalue":{"value":{"entity-type":"item","numeric-id":4913777,"id":"Q4913777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$F07C24B0-F548-4767-888F-15346DA1DB4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06eac9a890b9a94565701524b47651606e322438","datavalue":{"value":{"entity-type":"item","numeric-id":1763729,"id":"Q1763729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$93552A49-D44C-4E89-9C4B-A7AF39823F90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3692aa2d157356a2dba2cdcf8e4dfc8407c894b","datavalue":{"value":{"entity-type":"item","numeric-id":5452612,"id":"Q5452612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$28D3CCF1-7962-4B58-94EF-A0BD03CBCFE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2875da2348ba3de61abec02e7268276d1bf41d2e","datavalue":{"value":{"entity-type":"item","numeric-id":3512504,"id":"Q3512504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$0CAC4211-9168-4803-A19E-F7703FCC4149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b24b5b561cde7a5eef6f6e87df461bfda495bb00","datavalue":{"value":{"entity-type":"item","numeric-id":3773877,"id":"Q3773877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$5411A38E-D1D7-4706-AB81-0AA977A24E12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"947f377ca9b6bb3fda91c2ab02f06c0ede20fc8a","datavalue":{"value":{"entity-type":"item","numeric-id":1183580,"id":"Q1183580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$966F9854-2CB0-4BE2-A76C-64548CBDD122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fca8c6bae599173b38636aaeee9a044e8d5419f","datavalue":{"value":{"entity-type":"item","numeric-id":5311261,"id":"Q5311261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2417849$6A6E4D0C-CBF6-417D-B63F-8BD5BBD8F825","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e77e69f79f88ea9675f87dbc68e26109ddd0cc32","datavalue":{"value":"Q128273622","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$334D8FE4-309B-4DF3-AEF1-64EA26F9C708","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b8e7b4ba385ac49b306786ac03989a680386c8f5","datavalue":{"value":"10.1016/J.IC.2019.03.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2417849$8EBC1E35-E7D4-4C3C-B822-A0BF9F1CF81C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7745c71156ecdc53ab628c037baa8a9017ec16f1","datavalue":{"value":{"entity-type":"item","numeric-id":278747,"id":"Q278747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c147143373edeac7fd6728126a00ab9096e26a7","datavalue":{"value":{"amount":"+0.8476865291595459","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":"Q2417849$5AB42420-520F-4261-B549-280E31EB3BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0481f031154a8dd53d911682af117a071e4b93aa","datavalue":{"value":{"entity-type":"item","numeric-id":3179309,"id":"Q3179309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9e9c8a4b6ef1089584356199679d80636617d02","datavalue":{"value":{"amount":"+0.8180860877037048","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":"Q2417849$D26FBA1B-ADFC-45FD-8FAB-5CE06FE092CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45bc313aa76b16cbd2e41776b3eafe3b9544f590","datavalue":{"value":{"entity-type":"item","numeric-id":5277913,"id":"Q5277913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c86d34e12a64394a621e71104c6101c85402dcc","datavalue":{"value":{"amount":"+0.8122929930686951","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":"Q2417849$52B9800E-4D29-4B88-B749-C3454F0E8DF3","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":"3fe2b208282a06500be2ab01ed81b974bf29bf77","datavalue":{"value":{"amount":"+0.8045560717582703","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":"Q2417849$B556938A-2E6E-463E-8AF3-D6853FCF0D11","rank":"normal"},{"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":"83c9866acac433e28da1e567c5d7d5abaad49a3b","datavalue":{"value":{"amount":"+0.7961742877960205","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":"Q2417849$7708B12C-A0BF-4407-9D33-88E95B2C7697","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2417849","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2417849"}}}}}