Document Open Access Logo

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment

Authors Mnacho Echenim, Radu Iosif, Nicolas Peltier

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.20.pdf
  • Filesize: 0.62 MB
  • 18 pages

Document Identifiers

Author Details

Mnacho Echenim
  • Université Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France
Radu Iosif
  • Université Grenoble Alpes, CNRS, VERIMAG, F-38000 Grenoble, France
Nicolas Peltier
  • Université Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France

Cite AsGet BibTex

Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.20

Abstract

We define a class of Separation Logic [Ishtiaq and O'Hearn, 2001; J.C. Reynolds, 2002] formulae, whose entailment problem given formulae ϕ, ψ₁, …, ψ_n, is every model of ϕ a model of some ψ_i? is 2-EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work [Iosif et al., 2013; Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020] consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated location, i.e. from the domain of the heap. In particular, this guarantees that each structure has treewidth bounded by the size of the largest rule in the set. In contrast, here we show that establishment, although sufficient for decidability (alongside two other natural conditions), is not necessary, by providing a condition, called equational restrictedness, which applies syntactically to (dis-)equalities. The entailment problem is more general in this case, because equationally restricted rules define richer classes of structures, of unbounded treewidth. In this paper we show that (1) every established set of rules can be converted into an equationally restricted one and (2) the entailment problem is 2-EXPTIME-complete in the latter case, thus matching the complexity of entailments for established sets of rules [Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020].

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Separation logic
  • Induction definitions
  • Inductive theorem proving
  • Entailments
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Joël 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-425, 2014. Google Scholar
  2. Josh Berdine, Byron Cook, and Samin Ishtiaq. Slayer: Memory safety for systems-level code. In Ganesh Gopalakrishnan andShaz Qadeer, editor, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of LNCS, pages 178-183. Springer, 2011. Google Scholar
  3. Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, 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-29, 2015, Proceedings, volume 9058 of LNCS, pages 3-11. Springer, 2015. Google Scholar
  4. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. Google Scholar
  5. Kamil Dudka, Petr Peringer, and Tomás 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-20, 2011. Proceedings, volume 6806 of LNCS, pages 372-378. Springer, 2011. Google Scholar
  6. 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://easychair.org/publications/paper/DdNg.
  7. J. Flum and M. Grohe. Parameterized Complexity Theory. Springer-Verlag New York, Inc., 2006. Google Scholar
  8. 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
  9. 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 Lecture Notes in Computer Science, pages 201-218. Springer, 2014. Google Scholar
  10. 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. Google Scholar
  11. Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified reasoning about robustness properties of symbolic-heap separation logic. In Hongseok Yang, editor, Programming Languages and Systems (ESOP'17), pages 611-638. Springer Berlin Heidelberg, 2017. Google Scholar
  12. Jens Katelaan, Christoph Matheja, and Florian Zuleger. Effective entailment checking for separation logic with inductive definitions. In Tomás Vojnar and Lijun Zhang, editors, TACAS 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, pages 319-336. Springer, 2019. Google Scholar
  13. Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Cyclic Theorem Prover for Separation Logic by Magic Wand. In ADSL 18 (First Workshop on Automated Deduction for Separation Logics), July 2018. Oxford, United Kingdom. Google Scholar
  14. Jens Pagel, Christoph Matheja, and Florian Zuleger. Complete entailment checking for separation logic with inductive definitions, 2020. URL: http://arxiv.org/abs/2002.01202.
  15. 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-408. EasyChair, 2020. URL: https://easychair.org/publications/paper/VTGk.
  16. J.C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS'02, 2002. Google Scholar
  17. Neil Robertson and P.D Seymour. Graph minors. III. Planar tree-width. Journal of Combinatorial Theory, Series B, 36(1):49-64, 1984. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact