Document Open Access Logo

The Entailment Problem for Separation Logic with Overlaid Structures

Authors Lucas Bueri , Nicolas Peltier , Quentin Petitjean , Mihaela Sighireanu

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.94.pdf
  • Filesize: 0.89 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
Keywords
  • Decision Procedure
  • Separation Logic
  • Inductive Definitions
  • Overlaid Data Structures

Metrics

Abstract

Separation Logic (SL) enables reasoning about programs that manipulate pointers. Its key feature is the separating conjunction ⋆, which asserts that two formulas hold on disjoint portions of memory. We consider an extension of SL, called Overlaid SL (OSL), that allows non-disjoint combinations of data structures defined over different fields, enriched with set constraints on the nodes of these structures. We prove that entailment is decidable for a broad class of data structures satisfying the so-called PCE conditions of [Iosif et al., 2013], thus extending this result to OSL. Our decision procedure is nondeterministic with doubly exponential time complexity.

Cite As Get BibTex

Lucas Bueri, Nicolas Peltier, Quentin Petitjean, and Mihaela Sighireanu. The Entailment Problem for Separation Logic with Overlaid Structures. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 94:1-94:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.94

Author Details

Lucas Bueri
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France
Nicolas Peltier
  • Université Grenoble Alpes, CNRS, LIG, France
Quentin Petitjean
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France
Mihaela Sighireanu
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France

Funding

This work has been partially funded by the French National Research Agency project ANR-21-CE48-0011.

References

  1. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A decidable fragment of separation logic. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_9.
  2. Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. Local shape analysis for overlaid data structures. In Francesco Logozzo and Manuel Fähndrich, editors, Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 150-171. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38856-9_10.
  3. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 191-211. EasyChair, 2020. URL: https://doi.org/10.29007/F5WH.
  4. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.20.
  5. Marco Eilers, Malte Schwerhoff, and Peter Müller. Verification algorithms for automated separation logic verifiers. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 362-386. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_18.
  6. Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. In Jacques Garrigue, editor, Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science, pages 314-333. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-12736-1_17.
  7. Constantin Enea, Vlad Saveluc, and Mihaela Sighireanu. Compositional invariant checking for overlaid and nested linked lists. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 129-148. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_9.
  8. Aquinas Hobor and Jules Villard. The ramifications of sharing in data structures. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 523-536. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429131.
  9. Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The Tree Width of Separation Logic with Recursive Definitions. In Maria Paola Bonacina, editor, Automated Deduction – CADE-24, volume 7898 of Lecture Notes in Computer Science, pages 21-38, Berlin, Heidelberg, 2013. Springer. ISSN: 1611-3349. URL: https://doi.org/10.1007/978-3-642-38574-2_2.
  10. Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In Franck Cassez and Jean-François Raskin, editors, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pages 201-218. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11936-6_15.
  11. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 14-26, New York, NY, USA, January 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.375719.
  12. Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning, 36(3):213-239, April 2006. URL: https://doi.org/10.1007/s10817-006-9042-1.
  13. Oukseh Lee, Hongseok Yang, and Rasmus Petersen. Program Analysis for Overlaid Data Structures. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 592-608, Berlin, Heidelberg, 2011. Springer. URL: https://doi.org/10.1007/978-3-642-22110-1_48.
  14. Christoph Matheja, Jens Pagel, and Florian Zuleger. A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. ACM Transactions on Computational Logic, 24(1):1 : 1-76, January 2023. URL: https://doi.org/10.1145/3534927.
  15. Nicolas Peltier, Quentin Petitjean, and Mihaela Sighireanu. Deciding satisfiability for overlaid symbolic heaps. In René Thiemann and Christoph Weidenbach, editors, Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, volume 15979 of Lecture Notes in Computer Science, pages 80-97. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04167-8_5.
  16. J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74, Copenhagen, Denmark, July 2002. ISSN: 1043-6871. URL: https://doi.org/10.1109/LICS.2002.1029817.
  17. Asankhaya Sharma, Aquinas Hobor, and Wei-Ngan Chin. Specifying compatible sharing in data structures. In Proceedings of the 17th International Conference on Formal Methods and Software Engineering (ICFEM), Lecture Notes in Computer Science, pages 349-365. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25423-4_23.
  18. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the Complexity of Equational Horn Clauses. In Robert Nieuwenhuis, editor, Automated Deduction – CADE-20, volume 3632 of Lecture Notes in Computer Science, pages 337-352, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/11532231_25.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact