{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:49Z","timestamp":1772119609932,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T00:00:00Z","timestamp":1674000000000},"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. Comput. Logic"],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>We develop a doubly exponential decision procedure for the satisfiability problem of<jats:italic>guarded separation logic<\/jats:italic>\u2014a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the preceding connectives leads to an undecidable fragment.<\/jats:p><jats:p>We further apply our decision procedure to reason about<jats:italic>entailments<\/jats:italic>in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly exponential decision procedure for entailments between (quantifier-free) symbolic heaps with inductive predicate definitions of bounded treewidth (<jats:bold>SL<jats:sub>btw<\/jats:sub><\/jats:bold>)\u2014one of the most expressive decidable fragments of separation logic. Together with the recently shown<jats:sc>2ExpTime<\/jats:sc>-hardness for entailments in said fragment, we conclude that the entailment problem for<jats:bold>SL<jats:sub>btw<\/jats:sub><\/jats:bold>is<jats:sc>2ExpTime<\/jats:sc>-complete\u2014thereby closing a previously open complexity gap.<\/jats:p>","DOI":"10.1145\/3534927","type":"journal-article","created":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T11:22:02Z","timestamp":1663845722000},"page":"1-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"first","affiliation":[{"name":"Technical University of Denmark and ETH Zurich, Kgs Lyngby, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8211-767X","authenticated-orcid":false,"given":"Jens","family":"Pagel","sequence":"additional","affiliation":[{"name":"TU Wien, Wien, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"TU Wien, Wien, Austria"}]}],"member":"320","published-online":{"date-parts":[[2023,1,18]]},"reference":[{"key":"e_1_3_4_2_1","first-page":"411","volume-title":"Proceedings of FOSSACS\u201914","author":"Antonopoulos Timos","year":"2014","unstructured":"Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Jo\u00ebl Ouaknine. 2014. Foundations for decision problems in separation logic with general inductive predicates. In Proceedings of FOSSACS\u201914. 411\u2013425."},{"key":"e_1_3_4_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_4_4_1","first-page":"143","article-title":"On formal properties of simple phrase structure grammars","volume":"14","author":"Bar-Hillel Yehoshua","year":"1961","unstructured":"Yehoshua Bar-Hillel, Micha Perles, and Eli Shamir. 1961. On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung 14 (1961), 143\u2013172.","journal-title":"Sprachtypologie und Universalienforschung"},{"key":"e_1_3_4_5_1","first-page":"Article 34, 29","article-title":"Quantitative separation logic: A logic for reasoning about probabilistic pointer programs","volume":"3","author":"Batz Kevin","year":"2019","unstructured":"Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: A logic for reasoning about probabilistic pointer programs. Proceedings of the ACM on Programming Languages 3, POPL (2019), Article 34, 29 pages.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_4_6_1","first-page":"178","volume-title":"Proceedings of CAV\u201907","author":"Berdine Josh","year":"2007","unstructured":"Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O\u2019Hearn, Thomas Wies, and Hongseok Yang. 2007. Shape analysis for composite data structures. In Proceedings of CAV\u201907. 178\u2013192."},{"key":"e_1_3_4_7_1","first-page":"97","volume-title":"Proceedings of FSTTCS\u201904","author":"Berdine Josh","year":"2004","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2004. A decidable fragment of separation logic. In Proceedings of FSTTCS\u201904. 97\u2013109."},{"key":"e_1_3_4_8_1","first-page":"115","volume-title":"Proceedings of FMCO\u201905","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2005a. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of FMCO\u201905. 115\u2013137."},{"key":"e_1_3_4_9_1","first-page":"52","volume-title":"Proceedings of APLAS\u201905","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2005b. Symbolic execution with separation logic. In Proceedings of APLAS\u201905. 52\u201368."},{"key":"e_1_3_4_10_1","first-page":"178","volume-title":"Proceedings of CAV\u201911","author":"Berdine Josh","year":"2011","unstructured":"Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory safety for systems-level code. In Proceedings of CAV\u201911. 178\u2013183."},{"key":"e_1_3_4_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0372-3"},{"key":"e_1_3_4_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"e_1_3_4_13_1","doi-asserted-by":"crossref","unstructured":"James Brotherston. 2007. Formalised inductive reasoning in the logic of bunched implications. In Static Analysis . Lecture Notes in Computer Science Vol. 4634. Springer 87\u2013103.","DOI":"10.1007\/978-3-540-74061-2_6"},{"key":"e_1_3_4_14_1","first-page":"131","volume-title":"Proceedings of CADE\u201911","author":"Brotherston James","year":"2011","unstructured":"James Brotherston, Dino Distefano, and Rasmus Lerche dahl Petersen. 2011. Automated cyclic entailment proofs in separation logic. In Proceedings of CADE\u201911. 131\u2013146."},{"key":"e_1_3_4_15_1","first-page":"Article 25, 10","volume-title":"Proceedings of CSL-LICS\u201914","author":"Brotherston James","year":"2014","unstructured":"James Brotherston, Carsten Fuhs, Juan Antonio Navarro P\u00e9rez, and Nikos Gorogiannis. 2014. A decision procedure for satisfiability in separation logic with inductive predicates. In Proceedings of CSL-LICS\u201914. Article 25, 10 pages."},{"key":"e_1_3_4_16_1","first-page":"459","volume-title":"Proceedings of NFM\u201911","author":"Calcagno Cristiano","year":"2011","unstructured":"Cristiano Calcagno and Dino Distefano. 2011. Infer: An automatic program verifier for memory safety of C programs. In Proceedings of NFM\u201911. 459\u2013465."},{"key":"e_1_3_4_17_1","first-page":"3","volume-title":"Proceedings of NFM\u201915","author":"Calcagno Cristiano","year":"2015","unstructured":"Cristiano Calcagno, Dino Distefano, J\u00e9r\u00e9my Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dul ma Rodriguez. 2015. Moving fast with software verification. In Proceedings of NFM\u201915. 3\u201311."},{"key":"e_1_3_4_18_1","first-page":"182","volume-title":"Proceedings of SAS\u201906","author":"Calcagno Cristiano","year":"2006","unstructured":"Cristiano Calcagno, Dino Distefano, Peter W. O\u2019Hearn, and Hongseok Yang. 2006. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In Proceedings of SAS\u201906. 182\u2013203."},{"issue":"6","key":"e_1_3_4_19_1","first-page":"Article 26, 66","article-title":"Compositional shape analysis by means of bi-abduction","volume":"58","author":"Calcagno Cristiano","year":"2011","unstructured":"Cristiano Calcagno, Dino Distefano, Peter W. O\u2019Hearn, and Hongseok Yang. 2011. Compositional shape analysis by means of bi-abduction. Journal of the ACM 58, 6 (2011), Article 26, 66 pages.","journal-title":"Journal of the ACM"},{"key":"e_1_3_4_20_1","first-page":"366","volume-title":"Proceedings of LICS\u201907","author":"Calcagno Cristiano","year":"2007","unstructured":"Cristiano Calcagno, Peter W. O\u2019Hearn, and Hongseok Yang. 2007. Local action and abstract separation logic. In Proceedings of LICS\u201907. 366\u2013378."},{"key":"e_1_3_4_21_1","first-page":"289","volume-title":"Proceedings of APLAS\u201901","author":"Calcagno Cristiano","year":"2001","unstructured":"Cristiano Calcagno, Hongseok Yang, and Peter W. O\u2019Hearn. 2001. Computability and complexity results for a spatial assertion language for data structures. In Proceedings of APLAS\u201901. 289\u2013300."},{"key":"e_1_3_4_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_3_4_23_1","first-page":"235","volume-title":"Proceedings of CONCUR\u201911","author":"Cook Byron","year":"2011","unstructured":"Byron Cook, Christoph Haase, Jo\u00ebl Ouaknine, Matthew J. Parkinson, and James Worrell. 2011. Tractable reasoning in a fragment of separation logic. In Proceedings of CONCUR\u201911. 235\u2013249."},{"key":"e_1_3_4_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2414243"},{"key":"e_1_3_4_25_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_3_4_26_1","doi-asserted-by":"crossref","unstructured":"Reinhard Diestel. 2016. Graph Theory (5th ed.). Graduate Texts in Mathematics Vol. 173. Springer.","DOI":"10.1007\/978-3-662-53622-3_7"},{"issue":"3","key":"e_1_3_4_27_1","first-page":"Article 19, 46","article-title":"The Bernays-Sch\u00f6nfinkel-Ramsey class of separation logic with uninterpreted predicates","volume":"21","author":"Echenim Mnacho","year":"2020","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2020a. The Bernays-Sch\u00f6nfinkel-Ramsey class of separation logic with uninterpreted predicates. ACM Transactions on Computational Logic 21, 3 (2020), Article 19, 46 pages.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_4_28_1","doi-asserted-by":"crossref","unstructured":"Mnacho Echenim Radu Iosif and Nicolas Peltier. 2020b. Entailment checking in separation logic with inductive definitions is 2-EXPTIME hard. In Proceedings of LPAR\u201920 . 191\u2013211.","DOI":"10.29007\/f5wh"},{"key":"e_1_3_4_29_1","volume-title":"Proceedings of CSL\u201921.","author":"Echenim Mnacho","year":"2021","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2021. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In Proceedings of CSL\u201921."},{"key":"e_1_3_4_30_1","first-page":"302","volume-title":"Proceedings of NFM\u201917","author":"Enea Constantin","year":"2017","unstructured":"Constantin Enea, Ondrej Leng\u00e1l, Mihaela Sighireanu, and Tom\u00e1s Vojnar. 2017. SPEN: A solver for separation logic. In Proceedings of NFM\u201917. 302\u2013309."},{"key":"e_1_3_4_31_1","first-page":"266","volume-title":"Proceedings of PLDI\u201907","author":"Gotsman Alexey","year":"2007","unstructured":"Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv. 2007. Thread-modular shape analysis. In Proceedings of PLDI\u201907. 266\u2013277."},{"key":"e_1_3_4_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1454320"},{"key":"e_1_3_4_33_1","first-page":"21","volume-title":"Proceedings of CADE\u201913","author":"Iosif Radu","year":"2013","unstructured":"Radu Iosif, Adam Rogalewicz, and Jir\u00ed Sim\u00e1cek. 2013. The tree width of separation logic with recursive definitions. In Proceedings of CADE\u201913. 21\u201338."},{"key":"e_1_3_4_34_1","first-page":"201","volume-title":"Proceedings of ATVA\u201914","author":"Iosif Radu","year":"2014","unstructured":"Radu Iosif, Adam Rogalewicz, and Tom\u00e1s Vojnar. 2014. Deciding entailments in inductive separation logic with tree automata. In Proceedings of ATVA\u201914. 201\u2013218."},{"key":"e_1_3_4_35_1","first-page":"14","volume-title":"Proceedings of POPL\u201901","author":"Ishtiaq Samin S.","year":"2001","unstructured":"Samin S. Ishtiaq and Peter W. O\u2019Hearn. 2001. BI as an assertion language for mutable data structures. In Proceedings of POPL\u201901. 14\u201326."},{"key":"e_1_3_4_36_1","first-page":"41","volume-title":"Proceedings of NFM\u201911","author":"Jacobs Bart","year":"2011","unstructured":"Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of NFM\u201911. 41\u201355."},{"key":"e_1_3_4_37_1","first-page":"611","volume-title":"Proceedings of ESOP\u201917","author":"Jansen Christina","year":"2017","unstructured":"Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. 2017. Unified reasoning about robustness properties of symbolic-heap separation logic. In Proceedings of ESOP\u201917. 611\u2013638."},{"key":"e_1_3_4_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_4_39_1","first-page":"319","volume-title":"Proceedings of TACAS\u201919","author":"Katelaan Jens","year":"2019","unstructured":"Jens Katelaan, Christoph Matheja, and Florian Zuleger. 2019. Effective entailment checking for separation logic with inductive definitions. In Proceedings of TACAS\u201919. 319\u2013336."},{"key":"e_1_3_4_40_1","unstructured":"Jens Katelaan and Florian Zuleger. 2020. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Proceedings of LPAR\u201920 . 390\u2013408."},{"key":"e_1_3_4_41_1","first-page":"495","volume-title":"Proceedings of CAV\u201917","author":"Le Quang Loc","year":"2017","unstructured":"Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin. 2017. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proceedings of CAV\u201917. 495\u2013517."},{"key":"e_1_3_4_42_1","volume-title":"Automated Reasoning and Randomization in Separation Logic","author":"Matheja Christoph","year":"2020","unstructured":"Christoph Matheja. 2020. Automated Reasoning and Randomization in Separation Logic. Ph.D. Dissertation. RWTH Aachen University."},{"key":"e_1_3_4_43_1","first-page":"104","volume-title":"Dependable Software Systems Engineering","author":"M\u00fcller Peter","year":"2017","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2017. Viper: A verification infrastructure for permission-based reasoning. In Dependable Software Systems Engineering. IOS Press, 104\u2013125."},{"key":"e_1_3_4_44_1","article-title":"Complete entailment checking for separation logic with inductive definitions","volume":"2002","author":"Pagel Jens","year":"2020","unstructured":"Jens Pagel, Christoph Matheja, and Florian Zuleger. 2020. Complete entailment checking for separation logic with inductive definitions. CoRR abs\/2002.01202 (2020).","journal-title":"CoRR"},{"key":"e_1_3_4_45_1","first-page":"773","volume-title":"Proceedings of CAV\u201913","author":"Piskac Ruzica","year":"2013","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating separation logic using SMT. In Proceedings of CAV\u201913. 773\u2013789."},{"key":"e_1_3_4_46_1","first-page":"124","volume-title":"Proceedings of TACAS\u201914","author":"Piskac Ruzica","year":"2014","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014a. GRASShopper\u2014Complete heap verification with mixed specifications. In Proceedings of TACAS\u201914. 124\u2013139."},{"key":"e_1_3_4_47_1","first-page":"711","volume-title":"Proceedings of CAV\u201914","author":"Piskac Ruzica","year":"2014","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014b. Automating separation logic with trees and data. In Proceedings of CAV\u201914. 711\u2013728."},{"key":"e_1_3_4_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_4_49_1","first-page":"614","volume-title":"Proceedings of ECOOP\u201915","author":"Schwerhoff Malte","year":"2015","unstructured":"Malte Schwerhoff and Alexander J. Summers. 2015. Lightweight support for magic wands in an automatic verifier. In Proceedings of ECOOP\u201915. 614\u2013638."},{"key":"e_1_3_4_50_1","first-page":"Lecture Notes i","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Sighireanu Mihaela","year":"2019","unstructured":"Mihaela Sighireanu, Juan A. Navarro Perez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, et al.2019. SL-COMP: Competition of solvers for separation logic. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 11429. Springer, 116\u2013132."},{"key":"e_1_3_4_51_1","doi-asserted-by":"crossref","unstructured":"Quang-Trung Ta Ton Chanh Le Siau-Cheng Khoo and Wei-Ngan Chin. 2016. Automated mutual explicit induction proof in separation logic. In Formal Methods . Lecture Notes in Computer Science Vol. 9995. Springer 659\u2013676.","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_4_52_1","first-page":"Article 9, 29 p","article-title":"Automated lemma synthesis in symbolic-heap separation logic","volume":"2","author":"Ta Quang-Trung","year":"2018","unstructured":"Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2018. Automated lemma synthesis in symbolic-heap separation logic. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 9, 29 pages.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_4_53_1","first-page":"58","volume-title":"Proceedings of SPIN\u201914","author":"Thakur Aditya V.","year":"2014","unstructured":"Aditya V. Thakur, Jason Breck, and Thomas W. Reps. 2014. Satisfiability modulo abstraction for separation logic with linked lists. In Proceedings of SPIN\u201914. 58\u201367."},{"key":"e_1_3_4_54_1","volume-title":"Local Reasoning for Stateful Programs","author":"Yang Hongseok","year":"2001","unstructured":"Hongseok Yang. 2001. Local Reasoning for Stateful Programs. Ph.D. Dissertation. University of Illinois at Urbana\u2013Champaign, Champaign, IL."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534927","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3534927","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:53Z","timestamp":1750186973000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534927"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,18]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3534927"],"URL":"https:\/\/doi.org\/10.1145\/3534927","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,18]]},"assertion":[{"value":"2021-01-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-04-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}