{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T16:29:51Z","timestamp":1768408191293,"version":"3.49.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,3,2]],"date-time":"2020-03-02T00:00:00Z","timestamp":1583107200000},"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":[[2020,7,31]]},"abstract":"<jats:p>\n            This article investigates the satisfiability problem for Separation Logic with\n            <jats:italic>k<\/jats:italic>\n            record fields, with unrestricted nesting of separating conjunctions and implications. It focuses on prenex formul\u00e6 with a quantifier prefix in the language \u2203*\u2200* that contain uninterpreted (heap-independent) predicate symbols. In analogy with first-order logic, we call this fragment\n            <jats:italic>Bernays-Sch\u00f6nfinkel-Ramsey Separation Logic<\/jats:italic>\n            [BSR(SL\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sup>\n            )]. In contrast with existing work on Separation Logic, in which the universe of possible locations is assumed to be infinite, we consider both finite and infinite universes in the present article. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SL\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sup>\n            ). Then we define two non-trivial subsets thereof, for which the finite and infinite satisfiability problems are PSPACE-complete, respectively, assuming that the maximum arity of the uninterpreted predicate symbols does not depend on the input. These fragments are defined by controlling the polarity of the occurrences of separating implications, as well as the occurrences of universally quantified variables within their scope. These decidability results have natural applications in program verification, as they allow to automatically prove lemmas that occur in, e.g., entailment checking between inductively defined predicates and validity checking of Hoare triples expressing partial correctness conditions.\n          <\/jats:p>","DOI":"10.1145\/3380809","type":"journal-article","created":{"date-parts":[[2020,3,2]],"date-time":"2020-03-02T22:35:13Z","timestamp":1583188513000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["The Bernays-Sch\u00f6nfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates"],"prefix":"10.1145","volume":"21","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, LIG, Saint-Martin-d\u2019H\u00e8res"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Verimag, Saint-Martin-d\u2019H\u00e8res"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, LIG, Saint-Martin-d\u2019H\u00e8res"}]}],"member":"320","published-online":{"date-parts":[[2020,3,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Antonopoulos Timos","unstructured":"Timos Antonopoulos , Nikos Gorogiannis , Christoph Haase , Max Kanovich , and Jo\u00ebl Ouaknine . 2014. Foundations for decision problems in separation logic with general inductive predicates . In Foundations of Software Science and Computation Structures , Anca Muscholl (Ed.). Springer , Berlin , 411--425. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, and Jo\u00ebl Ouaknine. 2014. Foundations for decision problems in separation logic with general inductive predicates. In Foundations of Software Science and Computation Structures, Anca Muscholl (Ed.). Springer, Berlin, 411--425."},{"key":"e_1_2_1_2_1","volume-title":"Computational Complexity\u2014A Modern Approach","author":"Arora Sanjeev","unstructured":"Sanjeev Arora and Boaz Barak . 2009. Computational Complexity\u2014A Modern Approach . Cambridge University Press . Sanjeev Arora and Boaz Barak. 2009. Computational Complexity\u2014A Modern Approach. Cambridge University Press."},{"key":"e_1_2_1_3_1","volume-title":"The Classical Decision Problem","author":"B\u00f6rger Egon","unstructured":"Egon B\u00f6rger , Erich Gr\u00e4del , and Yuri Gurevich . 1997. The Classical Decision Problem . Springer . Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 1997. The Classical Decision Problem. Springer."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 23rd International Conference on Automated Deduction (CADE-23)","author":"Brotherston James","unstructured":"James Brotherston , Dino Distefano , and Rasmus L. Petersen . 2011. Automated cyclic entailment proofs in separation logic . In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23) . Springer, Berlin, 131--146. James Brotherston, Dino Distefano, and Rasmus L. Petersen. 2011. Automated cyclic entailment proofs in separation logic. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23). Springer, Berlin, 131--146."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_2_1_6_1","volume-title":"Foundations of Software Science and Computational Structures","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno , Philippa Gardner , and Matthew Hague . 2005. From separation logic to first-order logic . In Foundations of Software Science and Computational Structures . Springer , Berlin , 395--409. Cristiano Calcagno, Philippa Gardner, and Matthew Hague. 2005. From separation logic to first-order logic. In Foundations of Software Science and Computational Structures. Springer, Berlin, 395--409."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FST TCS\u201901)","author":"Calcagno Cristiano","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 the Conference on Foundations of Software Technology and Theoretical Computer Science (FST TCS\u201901) . Springer, Berlin, 108--119. 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 the Conference on Foundations of Software Technology and Theoretical Computer Science (FST TCS\u201901). Springer, Berlin, 108--119."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2835490"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"St\u00e9phane Demri \u00c9tienne Lozes and Alessio Mansutti. 2018. The effects of adding reachability predicates in propositional separation logic. In Proceedings of the 21st International Conference FOSSACS\u201918 held as part of the European Joint Conferences on Theory and Practice of Software Foundations of Software Science and Computation Structures (ETAPS\u201918) (Lecture Notes in Computer Science) Christel Baier and Ugo Dal Lago (Eds.) Vol. 10803. Springer 476--493.  St\u00e9phane Demri \u00c9tienne Lozes and Alessio Mansutti. 2018. The effects of adding reachability predicates in propositional separation logic. In Proceedings of the 21st International Conference FOSSACS\u201918 held as part of the European Joint Conferences on Theory and Practice of Software Foundations of Software Science and Computation Structures (ETAPS\u201918) (Lecture Notes in Computer Science) Christel Baier and Ugo Dal Lago (Eds.) Vol. 10803. Springer 476--493.","DOI":"10.1007\/978-3-319-89366-2_26"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_23"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.417"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of 4th International Verification Workshop in connection with (CADE-21)","volume":"259","author":"Fontaine Pascal","year":"2007","unstructured":"Pascal Fontaine . 2007 . Combinations of theories and the Bernays-Sch\u00f6nfinkel-ramsey class . In Proceedings of 4th International Verification Workshop in connection with (CADE-21) (CEUR Workshop Proceedings), Bernhard Beckert (Ed.) , Vol. 259 . CEUR-WS.org. Pascal Fontaine. 2007. Combinations of theories and the Bernays-Sch\u00f6nfinkel-ramsey class. In Proceedings of 4th International Verification Workshop in connection with (CADE-21) (CEUR Workshop Proceedings), Bernhard Beckert (Ed.), Vol. 259. CEUR-WS.org."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_2_1_14_1","volume-title":"O\u2019Hearn","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 ACM SIGPLAN Notices, Vol. 36 . ACM , 14--26. Samin S. Ishtiaq and Peter W. O\u2019Hearn. 2001. BI as an assertion language for mutable data structures. In ACM SIGPLAN Notices, Vol. 36. ACM, 14--26."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Jens Katelaan Christoph Matheja and Florian Zuleger. 2019. Effective entailment checking for separation logic with inductive definitions. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919) held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201919) Part II (Lecture Notes in Computer Science) Tom\u00e1s Vojnar and Lijun Zhang (Eds.) Vol. 11428. Springer 319--336.  Jens Katelaan Christoph Matheja and Florian Zuleger. 2019. Effective entailment checking for separation logic with inductive definitions. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919) held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201919) Part II (Lecture Notes in Computer Science) Tom\u00e1s Vojnar and Lijun Zhang (Eds.) Vol. 11428. Springer 319--336.","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE\u201904)","author":"Lozes Etienne","year":"2004","unstructured":"Etienne Lozes . 2004 . Separation logic preserves the expressive power of classical logic . In Proceedings of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE\u201904) . Etienne Lozes. 2004. Separation logic preserves the expressive power of classical logic. In Proceedings of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE\u201904)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_20_1","volume-title":"Computational Complexity","author":"Papadimitriou C. H.","unstructured":"C. H. Papadimitriou . 1994. Computational Complexity . Addison-Wesley . C. H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley."},{"key":"e_1_2_1_21_1","volume-title":"On a problem of formal logic. Classic Papers in Combinatorics","author":"Ramsey F. P.","year":"1987","unstructured":"F. P. Ramsey . 1987. On a problem of formal logic. Classic Papers in Combinatorics ( 1987 ), 1--24. F. P. Ramsey. 1987. On a problem of formal logic. Classic Papers in Combinatorics (1987), 1--24."},{"key":"e_1_2_1_22_1","volume-title":"Reasoning in the Bernays-Sch\u00f6nfinkel-Ramsey fragment of separation logic","author":"Reynolds Andrew","unstructured":"Andrew Reynolds , Radu Iosif , and Cristina Serban . 2017. Reasoning in the Bernays-Sch\u00f6nfinkel-Ramsey fragment of separation logic . In Verification, Model Checking, and Abstract Interpretation, Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing , Cham , 462--482. Andrew Reynolds, Radu Iosif, and Cristina Serban. 2017. Reasoning in the Bernays-Sch\u00f6nfinkel-Ramsey fragment of separation logic. In Verification, Model Checking, and Abstract Interpretation, Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing, Cham, 462--482."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 137--146","author":"Vardi Moshe Y.","year":"1982","unstructured":"Moshe Y. Vardi . 1982 . The complexity of relational query languages . In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 137--146 . Moshe Y. Vardi. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 137--146."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3380809","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3380809","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:06Z","timestamp":1750204386000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3380809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,2]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,7,31]]}},"alternative-id":["10.1145\/3380809"],"URL":"https:\/\/doi.org\/10.1145\/3380809","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3,2]]},"assertion":[{"value":"2019-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}