Document Open Access Logo

On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Author Nicolas Peltier

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.16.pdf
  • Filesize: 0.79 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Separation logic
  • Dynamic logic
  • Entailment problem

Metrics

Abstract

Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.

Cite As Get BibTex

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.16

Author Details

Nicolas Peltier
  • Univ. Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France

Funding

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

Acknowledgements

The author wishes to thank the anonymous referees for their valuable comments.

References

  1. J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. In Proc. of FSTTCS'04, volume 3328 of LNCS. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_9.
  2. James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 25:1-25:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603091.
  3. Cristiano Calcagno, Hongseok Yang, and Peter W O’hearn. Computability and complexity results for a spatial assertion language for data structures. In FST TCS 2001, Proceedings, pages 108-119. Springer, 2001. URL: https://doi.org/10.1007/3-540-45294-X_10.
  4. B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In Proc. of CONCUR'11, volume 6901 of LNCS. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_16.
  5. Frank S. de Boer, Hans-Dieter A. Hiep, and Stijn de Gouw. Dynamic separation logic. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023, volume 3 of EPTICS. EpiSciences, 2023. URL: https://doi.org/10.46298/ENTICS.12297.
  6. Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry. Separation logic with one quantified variable. In CSR'14, volume 8476 of LNCS, pages 125-138. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06686-8_10.
  7. 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.
  8. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. Inf. Process. Lett., 173:106169, 2022. URL: https://doi.org/10.1016/j.ipl.2021.106169.
  9. Mnacho Echenim and Nicolas Peltier. A proof procedure for separation logic with inductive definitions and data. J. Autom. Reason., 67(3):30, 2023. URL: https://doi.org/10.1007/S10817-023-09680-4.
  10. Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. Formal Methods Syst. Des., 51(3):575-607, 2017. URL: https://doi.org/10.1007/S10703-017-0289-4.
  11. Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In ATVA 2015, Proceedings, pages 80-96, 2015. URL: https://doi.org/10.1007/978-3-319-24953-7_7.
  12. 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. Google Scholar
  13. 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, ATVA 2014, Proceedings, volume 8837 of LNCS, pages 201-218. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11936-6_15.
  14. Samin S Ishtiaq and Peter W O'Hearn. Bi as an assertion language for mutable data structures. In ACM SIGPLAN Notices, volume 36, pages 14-26, 2001. URL: https://doi.org/10.1145/360204.375719.
  15. Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log., 24(1):1:1-1:76, 2023. URL: https://doi.org/10.1145/3534927.
  16. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of LNCS, pages 1-19. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  17. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  18. Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of LNCS, pages 367-387. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_19.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact