{"entities":{"Q707740":{"pageid":709589,"ns":120,"title":"Item:Q707740","lastrevid":63782850,"modified":"2026-04-11T15:30:55Z","type":"item","id":"Q707740","labels":{"en":{"language":"en","value":"Quantitative separation logic and programs with lists"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5797495"}},"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":"Q707740$011956A7-AB65-455D-BB6E-AC401F8BC4E4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8e0df54a15271f4ecbfcfe86956662572e0129d3","datavalue":{"value":{"text":"Quantitative separation logic and programs with lists","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q707740$2C513106-5AE2-4275-8B48-87E2C0C84FB6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"18c2da87ae6a10b6adea5cf894a6263aeab82d01","datavalue":{"value":"1207.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$F3154550-3BCD-4B8A-8F54-474775656461","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a20bf99fdb7ddd878f88c192741bf562f8917d0d","datavalue":{"value":{"entity-type":"item","numeric-id":537950,"id":"Q537950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$5C95B081-1312-4C8E-84CD-FCE608ED98D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ffdbfd7b9177bc6559af43c12c896a5d2e47038","datavalue":{"value":{"entity-type":"item","numeric-id":537951,"id":"Q537951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$21E2FF6C-942E-4722-9D73-6D9366884A86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c43112df2a06a4f3b39f7eebcad25eb5a17a745","datavalue":{"value":{"entity-type":"item","numeric-id":707739,"id":"Q707739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$402CEF70-9873-4582-B8F1-2FFC7BE93762","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$6A014534-EBB6-4E27-89C3-AEFD8E5B6966","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"12116120e612da11bd56798b90a3c232b35a10bb","datavalue":{"value":{"time":"+2010-10-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q707740$CAABE301-A419-4DD8-B165-217CD0858CA0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"62bd4628e7d9aa6341fee05dfb5d3c9fc477895e","datavalue":{"value":"An extension of a decidable fragment of Separation Logic for singly-linked lists is presented. The main extension consists in introducing atomic formulae of the form \\(ks^k(x,y)\\) describing a list segment of length \\(k\\), stretching from \\(x\\) to \\(y\\), where \\(k\\) is a logical variable interpreted over positive natural numbers, that occur further inside Presburger constraints. The decidability of the full first-order logic combining unrestricted quantification of arithmetic and location variables is studied. Although the full logic is undecidable, validity of entailments between formulae with the quantifier prefix in the language \\(\\exists^*\\{\\exists_{\\mathbb N}, \\forall_{\\mathbb N}\\}^*\\) is decidable. The decision technique, providing a fully automated framework for the verification of quantitative properties expressed as pre- and post- conditions on programs working lists and integer counters, is implemented.","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$AEB3BC5F-E5EF-4DB0-8517-6DE0C571F1C1","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"773908fafc294c05eb3467ec5d713b5469e8b7b3","datavalue":{"value":{"entity-type":"item","numeric-id":590927,"id":"Q590927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$1A3FD5B6-2043-4E0C-BF41-862F2AF15EFD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$ED804B45-41A9-4786-8C90-5507AEF0EE9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$E70758F9-B6F7-471A-B345-02C9C0B07366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$C9118031-D73B-4EAE-8F4B-48B8C56944B4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"013d8281fb3f1078cf1035008aa1c824f6a87aff","datavalue":{"value":"5797495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$4621FCB3-51B8-4BD4-BF74-561A9F6E9447","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$9BD1AE86-2339-4DE4-9F25-98BD334F5F3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$6EC893E6-EC6A-4FFD-A8BA-02F91C8E89BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac83e60b62a45eb5c56f20ea081f46512f234dd0","datavalue":{"value":"Presburger constraint","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$ACFAAA7A-2BAC-4601-A50C-44B05DD69534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"044a0b91eea67a5cd7e3eb152d3d61e9c6193fb8","datavalue":{"value":"list structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$FB315282-813E-4EAF-82D6-D4AD41F1806F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q707740$6BD51CAB-0C59-4FA6-BC1D-D8C2811667A1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ce91c9303e62db122d4c0c98d17eb9dbb9274541","datavalue":{"value":{"entity-type":"item","numeric-id":33078,"id":"Q33078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$293A3159-7FF5-44C2-9448-58961AA25C5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dc9e88abc913a4b4fba265878f62bb009e36efad","datavalue":{"value":{"entity-type":"item","numeric-id":17099,"id":"Q17099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$1681AF9C-EA65-4B40-9927-B734115436D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"630858108012d4b1d813d05f96b53442397f2dc9","datavalue":{"value":{"entity-type":"item","numeric-id":17101,"id":"Q17101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$FA62FDF5-7D72-46D9-99D1-FAEF7DCF6AF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb600505726038dde1f7205c06067efdfd1bd64e","datavalue":{"value":{"entity-type":"item","numeric-id":14127,"id":"Q14127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$6AAB671B-792F-479D-8DAE-F9A2F4D624B1","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":"Q707740$10EAB079-C7F8-4FBC-A79A-8C0A3ED7A330","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b31f53a0d0bde91edfb7e0c78ab601e4c924d89c","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9179-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q707740$49067726-501E-4980-93EA-E0143305CE64","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7ba549d1409b3fa64a8df593df08c9e7ff16e969","datavalue":{"value":"W2055411475","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$8D93C7D1-A1BE-4810-B4B2-25A830C0177C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"95df9aedbd7e5e563158d002f148b701b2fd0480","datavalue":{"value":{"entity-type":"item","numeric-id":4551165,"id":"Q4551165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$0DCB7394-02CF-4844-82A1-77142BBB0E71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c642b8a2a51ea751f61c4db5e751f89086f5237","datavalue":{"value":{"entity-type":"item","numeric-id":5465888,"id":"Q5465888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$479F0338-D8D8-4155-BBD6-D703B343FEDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee4a364c7ffd575e9526a9a72ed0402273dd4826","datavalue":{"value":{"entity-type":"item","numeric-id":5756740,"id":"Q5756740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$A9172159-CFBE-4CF9-BC94-44AA0847556B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c3a32751a143a211da73fec4c2725da5321c9d9","datavalue":{"value":{"entity-type":"item","numeric-id":3184673,"id":"Q3184673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$D715D168-319D-4795-A6D7-1C96B6F65167","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"454f7ae21f81dd356823b4e6d4bc77d27e5f3c29","datavalue":{"value":{"entity-type":"item","numeric-id":3540188,"id":"Q3540188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$A0782283-555A-4B64-B0CB-A6D55EA0CB88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16df2553495bc38f714aaa2197b34e11b69c06ef","datavalue":{"value":{"entity-type":"item","numeric-id":5674963,"id":"Q5674963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$3A89FAD2-2B9D-4BFF-B64B-99E7DF5FEC22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da55e362c0b7a7f678d0a3c4dbd5137695c17e6f","datavalue":{"value":{"entity-type":"item","numeric-id":5429331,"id":"Q5429331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$24E5F40D-84FC-4BD2-9BDA-AF2E93064D9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e1040f5d7de42f2064718e38c58ade083ef9993","datavalue":{"value":{"entity-type":"item","numeric-id":5312907,"id":"Q5312907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$BA34A65E-A7AA-4FC1-B3FF-3662465C0187","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":"Q707740$7360CC19-CA03-4CBC-B9EA-62C2194A466A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0622ab6665580df90f2ea4b5dedce67390824528","datavalue":{"value":{"entity-type":"item","numeric-id":3612011,"id":"Q3612011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$BD4620FE-4104-49E3-88C7-3BEA017735EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4b1d274c6ee4b9c24930fb83b43c12797e99121","datavalue":{"value":{"entity-type":"item","numeric-id":5590814,"id":"Q5590814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$83AC62C3-4B23-4934-AE8F-51BD68B6D418","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29ef7590ac163e04f88fc79c8e41f44e7fea181f","datavalue":{"value":{"entity-type":"item","numeric-id":4474211,"id":"Q4474211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$A54968B9-5156-45B0-9DAF-F38F98B4447F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"041f425d2424dea3c24ef7c01081663e6200bc4b","datavalue":{"value":{"entity-type":"item","numeric-id":5191097,"id":"Q5191097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$687C497E-432F-41F7-981D-A139EA2ABA5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01893115d15c8b27d6dde25c7a72d7981bc7bba4","datavalue":{"value":{"entity-type":"item","numeric-id":5899082,"id":"Q5899082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$FA38CA38-8CFE-44A8-A989-021F87AFB689","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"653533a466bb7480e50c4f2777f5ad26823d7154","datavalue":{"value":{"entity-type":"item","numeric-id":2432767,"id":"Q2432767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q707740$7E86C53A-F489-4C3C-82DB-AF3BCDB69739","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3d58d9887031b9f4fc1494af9b46408c8fa10801","datavalue":{"value":"10.1007/S10817-010-9179-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q707740$6CC37D41-3FE6-4944-8DAD-0434C9D08B61","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edba1fbe0d58190327dad32a688aad194871ddad","datavalue":{"value":{"entity-type":"item","numeric-id":3541685,"id":"Q3541685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecbbdcf44129d4cff052609afcea7c2b3cc11841","datavalue":{"value":{"amount":"+0.9976547360420228","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":"Q707740$BAF272BD-6D11-4B12-8B4B-94F8E108CE17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbd92fcbd187999428755f3015a6c0079f87cfd3","datavalue":{"value":{"entity-type":"item","numeric-id":5465888,"id":"Q5465888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8683d8b331a2236c2f590d51db77bced6d157bf6","datavalue":{"value":{"amount":"+0.8538948893547058","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":"Q707740$637F64E1-D833-40D8-913A-2E5FBD74B299","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52602e26599bc1b45617c5551d70aa6cdbfffb90","datavalue":{"value":{"entity-type":"item","numeric-id":3617745,"id":"Q3617745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97927c3c1140aa69f7387206a2660050569b9583","datavalue":{"value":{"amount":"+0.7931740880012512","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":"Q707740$0551C866-9FF2-439A-9002-390D936C99B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95daf92324fdba8c20ae3d08c2c86b375db37626","datavalue":{"value":{"entity-type":"item","numeric-id":1653010,"id":"Q1653010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bea7bfb4fc2ce09165caa1e1c40700b4c4a2b63","datavalue":{"value":{"amount":"+0.7926921248435974","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":"Q707740$FB7CA466-090C-4311-A749-E73F47A40CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99028e52e84438dcd63941e20ddc069a71aa9ca8","datavalue":{"value":{"entity-type":"item","numeric-id":4981154,"id":"Q4981154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4acecffac398698e8911f3dd34a151c4e6e1d61c","datavalue":{"value":{"amount":"+0.7894867658615112","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":"Q707740$6870A349-1F14-438C-A64A-8F4324C7B262","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantitative separation logic and programs with lists","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantitative_separation_logic_and_programs_with_lists"}}}}}