Tractability of Separation Logic with Inductive Definitions: Beyond Lists

Authors Taolue Chen, Fu Song, Zhilin Wu



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.37.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Taolue Chen
Fu Song
Zhilin Wu

Cite As Get BibTex

Taolue Chen, Fu Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.37

Abstract

In 2011, Cook et al. showed that the satisfiability and entailment  can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.

Subject Classification

Keywords
  • Separation logic
  • Inductive definitions
  • Satisfiability
  • Entailment

Metrics

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

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 FoSSaCS 2014, pages 411-425, 2014. Google Scholar
  2. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A decidable fragment of separation logic. In FSTTCS 2004, pages 97-109, 2004. Google Scholar
  3. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution with separation logic. In APLAS 2005, pages 52-68, 2005. Google Scholar
  4. Rémi Brochenin, Stéphane Demri, and Étienne Lozes. On the almighty wand. Inf. Comput., 211:106-137, 2012. Google Scholar
  5. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In CADE 2011, pages 131-146, 2011. Google Scholar
  6. James Brotherston, Carsten Fuhs, Juan A. Navarro Perez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In LICS 2014, pages 25:1-25:10, 2014. Google Scholar
  7. James Brotherston, Nikos Gorogiannis, and Max I. Kanovich. Biabduction (and related problems) in array separation logic. CoRR, abs/1607.01993, 2016. URL: http://arxiv.org/abs/1607.01993.
  8. James Brotherston, Nikos Gorogiannis, Max I. Kanovich, and Reuben Rowe. Model checking for symbolic-heap separation logic with inductive predicates. In POPL 2016, pages 84-96, 2016. Google Scholar
  9. Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In NFM 2011, pages 459-465, 2011. Google Scholar
  10. 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 NFM 2015, pages 3-11, 2015. Google Scholar
  11. Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and complexity results for a spatial assertion language for data structures. In FSTTCS 2001, pages 108-119, 2001. Google Scholar
  12. Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program., 77(9):1006-1036, 2012. URL: http://dx.doi.org/10.1016/j.scico.2010.07.004.
  13. Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. Automatic induction proofs of data-structures in imperative programs. In PLDI 2015, pages 457-466, 2015. Google Scholar
  14. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR 2011, pages 235-249, 2011. Google Scholar
  15. Stéphane Demri and Morgan Deters. Expressive completeness of separation logic with two variables and no separating conjunction. ACM Trans. Comput. Log., 17(2):12, 2016. Google Scholar
  16. Constantin Enea, Ondřej Lengál, Mihaela Sighireanu, and Tomáš Vojnar. Compositional entailment checking for a fragment of separation logic. In APLAS 2014, pages 314-333, 2014. Google Scholar
  17. Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In ATVA 2015, pages 80-96, 2015. Google Scholar
  18. Xincai Gu, Taolue Chen, and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints. In IJCAR 2016, pages 532-549, 2016. Google Scholar
  19. Christoph Haase, Samin Ishtiaq, Joël Ouaknine, and Matthew J. Parkinson. Seloger: A tool for graph-based reasoning in separation logic. In CAV 2013, pages 790-795, 2013. Google Scholar
  20. Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In CADE 2013, pages 21-38, 2013. Google Scholar
  21. Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In ATVA 2014, pages 201-218, 2014. Google Scholar
  22. Quang Loc Le, Jun Sun, and Wei-Ngan Chin. Satisfiability modulo heap-based programs. In CAV 2016, pages 382-404, 2016. Google Scholar
  23. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL 2001, pages 1-19, 2001. Google Scholar
  24. Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A decision procedure for separation logic in SMT. In ATVA 2016, pages 244-261, 2016. Google Scholar
  25. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 2002, pages 55-74, 2002. Google Scholar
  26. Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin. Decision procedure for separation logic with inductive definitions and presburger arithmetic. In APLAS 2016, pages 423-443, 2016. Google Scholar
  27. Zhaowei Xu, Taolue Chen, and Zhilin Wu. Satisfiability of compositional separation logic with tree predicates and data constraints. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 509-527. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-63046-5_31.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail