Document Open Access Logo

Extending Propositional Separation Logic for Robustness Properties

Author Alessio Mansutti

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.42.pdf
  • Filesize: 0.69 MB
  • 23 pages

Document Identifiers

Author Details

Alessio Mansutti
  • LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, Cachan, France

Cite AsGet BibTex

Alessio Mansutti. Extending Propositional Separation Logic for Robustness Properties. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.42

Abstract

We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
Keywords
  • Separation logic
  • decision problems
  • reachability
  • logics on trees
  • interval temporal logic
  • adjuncts and quantifiers elimination

Metrics

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

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, volume 8412 of Lecture Notes in Computer Science, pages 411-425. Springer, 2014. Google Scholar
  2. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In FMCO, volume 4111 of Lecture Notes in Computer Science, pages 115-137. Springer, 2005. Google Scholar
  3. Josh Berdine, Byron Cook, and Samin Ishtiaq. SLAyer: Memory Safety for Systems-Level Code. In CAV, volume 6806 of Lecture Notes in Computer Science, pages 178-183. Springer, 2011. 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. Luís Caires and Luca Cardelli. A Spatial Logic for Concurrency. In TACS, volume 2215 of Lecture Notes in Computer Science, pages 1-37. Springer, 2001. Google Scholar
  6. Cristiano Calcagno and Dino Distefano. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 459-465. Springer, 2011. Google Scholar
  7. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM, 58(6):26:1-26:66, 2011. Google Scholar
  8. Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In FSTTCS, volume 2245 of Lecture Notes in Computer Science, pages 108-119. Springer, 2001. Google Scholar
  9. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable Reasoning in a Fragment of Separation Logic. In CONCUR, volume 6901 of Lecture Notes in Computer Science, pages 235-249. Springer, 2011. Google Scholar
  10. Anuj Dawar, Philippa Gardner, and Giorgio Ghelli. Adjunct Elimination Through Games in Static Ambient Logic. In FSTTCS, volume 3328 of Lecture Notes in Computer Science, pages 211-223. Springer, 2004. Google Scholar
  11. Stéphane Demri and Morgan Deters. Two-Variable Separation Logic and Its Inner Circle. ACM Trans. Comput. Log., 16(2):15:1-15:36, 2015. Google Scholar
  12. Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry. Separation Logic with One Quantified Variable. Theory Comput. Syst., 61(2):371-461, 2017. Google Scholar
  13. Stéphane Demri, Étienne Lozes, and Alessio Mansutti. The Effects of Adding Reachability Predicates in Propositional Separation Logic. In FoSSaCS, volume 10803 of Lecture Notes in Computer Science, pages 476-493. Springer, 2018. Google Scholar
  14. Kamil Dudka, Petr Peringer, and Tomás Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In CAV, volume 6806 of Lecture Notes in Computer Science, pages 372-378. Springer, 2011. Google Scholar
  15. Christoph Haase, Samin Ishtiaq, Joël Ouaknine, and Matthew J. Parkinson. SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 790-795. Springer, 2013. Google Scholar
  16. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Commun. ACM, 12(10):576-580, 1969. Google Scholar
  17. Radu Iosif, Adam Rogalewicz, and Jirí Simácek. The Tree Width of Separation Logic with Recursive Definitions. In CADE, volume 7898 of Lecture Notes in Computer Science, pages 21-38. Springer, 2013. Google Scholar
  18. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 41-55. Springer, 2011. Google Scholar
  19. Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. In ESOP, volume 10201 of Lecture Notes in Computer Science, pages 611-638. Springer, 2017. Google Scholar
  20. Jens Katelaan, Dejan Jovanovic, and Georg Weissenbacher. A Separation Logic with Data: Small Models and Automation. In IJCAR, volume 10900 of Lecture Notes in Computer Science, pages 455-471. Springer, 2018. Google Scholar
  21. Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pages 495-517. Springer, 2017. Google Scholar
  22. Étienne Lozes. Adjuncts elimination in the static ambient logic. Electr. Notes Theor. Comput. Sci., 96:51-72, 2004. Google Scholar
  23. Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay. THOR: A tool for reasoning about shape and arithmetic. In CAV, volume 5123 of Lecture Notes in Computer Science, pages 428-432. Springer, 2008. Google Scholar
  24. Ben C. Moszkowski. A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time. Journal of Applied Non-Classical Logics, 14(1-2):55-104, 2004. Google Scholar
  25. Benjamin Charles Moszkowski. Reasoning About Digital Circuits. PhD thesis, Stanford University, Stanford, CA, USA, 1983. Google Scholar
  26. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, pages 55-74. IEEE Computer Society, 2002. Google Scholar
  27. Walter J. Savitch. Relationships Between Nondeterministic and Deterministic Tape Complexities. J. Comput. Syst. Sci., 4(2):177-192, 1970. Google Scholar
  28. Sylvain Schmitz. Complexity Hierarchies beyond Elementary. TOCT, 8(1):3:1-3:36, 2016. Google Scholar
  29. Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Scalable Shape Analysis for Systems Code. In CAV, volume 5123 of Lecture Notes in Computer Science, pages 385-398. Springer, 2008. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact