{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:25:46Z","timestamp":1772119546935,"version":"3.50.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The entailment problem<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\upvarphi \\models \\uppsi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03c6<\/mml:mi><mml:mo>\u22a7<\/mml:mo><mml:mi>\u03c8<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>in Separation Logic [12, 15], between separated conjunctions of equational (<jats:inline-formula><jats:alternatives><jats:tex-math>$$x \\approx y$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>x<\/mml:mi><mml:mo>\u2248<\/mml:mo><mml:mi>y<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and<jats:inline-formula><jats:alternatives><jats:tex-math>$$x \\not \\approx y$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>x<\/mml:mi><mml:mo>\u2249<\/mml:mo><mml:mi>y<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>), spatial (<jats:inline-formula><jats:alternatives><jats:tex-math>$$x \\mapsto (y_1,\\ldots ,y_\\upkappa )$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>x<\/mml:mi><mml:mo>\u21a6<\/mml:mo><mml:mo>(<\/mml:mo><mml:msub><mml:mi>y<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>,<\/mml:mo><mml:mo>\u2026<\/mml:mo><mml:mo>,<\/mml:mo><mml:msub><mml:mi>y<\/mml:mi><mml:mi>\u03ba<\/mml:mi><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) and predicate (<jats:inline-formula><jats:alternatives><jats:tex-math>$$p(x_1,\\ldots ,x_n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>p<\/mml:mi><mml:mo>(<\/mml:mo><mml:msub><mml:mi>x<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>,<\/mml:mo><mml:mo>\u2026<\/mml:mo><mml:mo>,<\/mml:mo><mml:msub><mml:mi>x<\/mml:mi><mml:mi>n<\/mml:mi><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called<jats:italic>establishment<\/jats:italic>[10, 13, 14] and<jats:italic>restrictedness<\/jats:italic>[8], respectively. Both classes are shown to be in<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {2\\text {EXPTIME}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mn>2<\/mml:mn><mml:mtext>EXPTIME<\/mml:mtext><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>by the independent proofs from [14] and [8], respectively, and a many-one reduction of established to restricted entailment problems has been given [8]. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left- (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\upvarphi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c6<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) and the right- (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\uppsi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c8<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) hand side of entailments, respectively. We provide a many-one reduction of this generalized class, called<jats:italic>safe<\/jats:italic>, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified,<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {2\\text {EXPTIME}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mn>2<\/mml:mn><mml:mtext>EXPTIME<\/mml:mtext><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-complete class.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_11","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"183-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Unifying Decidable Entailments in Separation Logic with Inductive Definitions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5765-0758","authenticated-orcid":false,"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3204-3294","authenticated-orcid":false,"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-7000","authenticated-orcid":false,"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Jo\u00ebl Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Anca Muscholl, editor, FOSSACS 2014, ETAPS 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 411\u2013425, 2014.","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"11_CR2","unstructured":"Josh Berdine, Byron Cook, and Samin Ishtiaq. Slayer: Memory safety for systems-level code. In Ganesh Gopalakrishnan and Shaz Qadeer, editor, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, volume 6806 of LNCS, pages 178\u2013183. Springer, 2011."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Dino Distefano, J\u00e9r\u00e9my Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27\u201329, 2015, Proceedings, volume 9058 of LNCS, pages 3\u201311. Springer, 2015.","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. Automatic induction proofs of data-structures in imperative programs. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pages 457\u2013466. ACM, 2015. URL: https:\/\/doi.org\/10.1145\/2737924.2737984, doi: $$\\text{10.1145\/2737924.2737984}$$.","DOI":"10.1145\/2737924.2737984"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Kamil Dudka, Petr Peringer, and Tom\u00e1s Vojnar. Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, volume 6806 of LNCS, pages 372\u2013378. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_29"},{"key":"11_CR6","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22\u201327, 2020, volume 73 of EPiC Series in Computing, pages 191\u2013211. EasyChair, 2020."},{"key":"11_CR7","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules. working paper or preprint, September 2020. URL: https:\/\/hal.archives-ouvertes.fr\/hal-02951630."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Echenim, Mnacho, Iosif, Radu, Peltier, Nicolas, Decidable entailments in separation logic with inductive definitions: Beyond establishment. In CSL 2021: 29th International Conference on Computer Science Logic, EPiC Series in Computing. EasyChair, 2021.","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Unifying decidable entailments in separation logic with inductive definitions, 2021. arXiv:2012.14361.","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In Proc. of CADE-24, volume 7898 of LNCS, 2013.","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Radu Iosif, Adam Rogalewicz, and Tom\u00e1s Vojnar. Deciding entailments in inductive separation logic with tree automata. In Franck Cassez and Jean-Fran\u00e7ois Raskin, editors, ATVA 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pages 201\u2013218. Springer, 2014.","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Samin S Ishtiaq and Peter W O\u2019Hearn. Bi as an assertion language for mutable data structures. In ACM SIGPLAN Notices, volume 36, pages 14\u201326, 2001","DOI":"10.1145\/373243.375719"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Jens Katelaan, Christoph Matheja, and Florian Zuleger. Effective entailment checking for separation logic with inductive definitions. In Tom\u00e1s Vojnar and Lijun Zhang, editors, TACAS 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, pages 319\u2013336. Springer, 2019.","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"11_CR14","unstructured":"Jens Pagel and Florian Zuleger. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In LPAR-23, volume 73 of EPiC Series in Computing, pages 390\u2013408. EasyChair, 2020."},{"key":"11_CR15","unstructured":"J.C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS\u201902, 2002"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. Automated lemma synthesis in symbolic-heap separation logic. Proc. ACM Program. Lang., 2(POPL):9:1\u20139:29, 2018. URL: https:\/\/doi.org\/10.1145\/3158097, doi: $$\\text{10.1145\/3158097 }$$.","DOI":"10.1145\/3158097"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:26:26Z","timestamp":1672723586000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}