{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T22:57:51Z","timestamp":1768431471772,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T00:00:00Z","timestamp":1657843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2022,9,30]]},"abstract":"<jats:p>Most automated verifiers for separation logic are based on the symbolic-heap fragment, which disallows both the magic-wand operator and the application of classical Boolean operators to spatial formulas. This is not surprising, as support for the magic wand quickly leads to undecidability, especially when combined with inductive predicates for reasoning about data structures. To circumvent these undecidability results, we propose assigning a more restrictive semantics to the separating conjunction. We argue that the resulting logic, strong-separation logic, can be used for symbolic execution and abductive reasoning just like \u201cstandard\u201d separation logic, while remaining decidable even in the presence of both the magic wand and inductive predicates (we consider a list-segment predicate and a tree predicate)\u2014a combination of features that leads to undecidability for the standard semantics.<\/jats:p>","DOI":"10.1145\/3498847","type":"journal-article","created":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T21:25:53Z","timestamp":1645651553000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Strong-separation Logic"],"prefix":"10.1145","volume":"44","author":[{"given":"Jens","family":"Pagel","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,7,15]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_15"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0372-3"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_10"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603142"},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06686-8_10"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_26"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_29"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_14"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434286"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_7"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_36"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_30"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"e_1_3_3_32_1","series-title":"Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning","first-page":"390","volume":"73","author":"Katelaan Jens","year":"2020","unstructured":"Jens Katelaan and Florian Zuleger. 2020. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(EPiC Series in Computing, Vol. 73), Elvira Albert and Laura Kov\u00e1cs (Eds.). EasyChair, 390\u2013408."},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_3_3_34_1","unstructured":"Siddharth Krishna Alexander J. Summers and Thomas Wies. 2019. Local reasoning for global graph properties. Retrieved from http:\/\/arxiv.org\/abs\/1911.08632."},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_12"},{"key":"e_1_3_3_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926455"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_3_39_1","unstructured":"Jens Pagel Christoph Matheja and Florian Zuleger. 2020. Complete entailment checking for separation logic with inductive definitions. Retrieved from https:\/\/arxiv.org\/abs\/2002.01202."},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_24"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"e_1_3_3_42_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"Piskac Ruzica","year":"2013","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating separation logic using SMT. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Lecture Notes in Computer Science, Vol. 8044. Springer, Berlin, 773\u2013789."},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_3_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_25"},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_3_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.614"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_5"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498847","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498847","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:08Z","timestamp":1750193348000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498847"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,15]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9,30]]}},"alternative-id":["10.1145\/3498847"],"URL":"https:\/\/doi.org\/10.1145\/3498847","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,15]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}