Document Open Access Logo

Internal Calculi for Separation Logics

Authors Stéphane Demri, Etienne Lozes, Alessio Mansutti

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.19.pdf
  • Filesize: 0.73 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Separation logic
  • internal calculus
  • adjunct/quantifier elimination

Metrics

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

Abstract

We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(∗, -*). We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.

Cite As Get BibTex

Stéphane Demri, Etienne Lozes, and Alessio Mansutti. Internal Calculi for Separation Logics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.19

Author Details

Stéphane Demri
  • LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
Etienne Lozes
  • Université Côte d’Azur, CNRS, I3S, France
Alessio Mansutti
  • LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France

Acknowledgements

We would like to thank the anonymous reviewers for their suggestions and remarks that help us to improve the quality of this paper.

References

  1. C. Areces, P. Blackburn, and M. Marx. Hybrid logics: characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3):977-1010, 2001. Google Scholar
  2. J. Berdine, C. Calcagno, and P.W. O'Hearn. A decidable fragment of separation logic. In FST&TCS'04, volume 3328 of LNCS, pages 97-109. Springer, 2004. Google Scholar
  3. M. Bozga, R. Iosif, and S. Perarnau. Quantitative Separation Logic and Programs with Lists. Journal of Automated Reasoning, 45(2):131-156, 2010. Google Scholar
  4. R. Brochenin, S. Demri, and E. Lozes. On the Almighty Wand. Information and Computation, 211:106-137, 2012. Google Scholar
  5. J. Brotherston. Bunched Logics Displayed. Studia Logica, 100(6):1223-1254, 2012. URL: https://doi.org/10.1007/s11225-012-9449-0.
  6. J. Brotherston and M. Kanovich. Undecidability of Propositional Separation Logic and Its Neighbours. Journal of the Association for Computing Machinery, 61(2), 2014. Google Scholar
  7. J. Brotherston and M. Kanovich. On the Complexity of Pointer Arithmetic in Separation Logic. In APLAS'18, volume 11275 of LNCS, pages 329-349. Springer, 2018. Google Scholar
  8. J. Brotherston and J. Villard. Parametric completeness for separation theories. In POPL'14, pages 453-464. ACM, 2014. Google Scholar
  9. C. Calcagno, Ph. Gardner, and M. Hague. From separation logic to first-order logic. In FoSSaCS'05, volume 3441 of LNCS, pages 395-409. Springer, 2005. Google Scholar
  10. C. Calcagno, P.W. O'Hearn, and H. Yang. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In FST&TCS'01, volume 2245 of LNCS, pages 108-119. Springer, 2001. Google Scholar
  11. B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable Reasoning in a Fragment of Separation Logic. In CONCUR'11, volume 6901 of LNCS, pages 235-249. Springer, 2011. Google Scholar
  12. S. Demri and M. Deters. Separation Logics and Modalities: A Survey. Journal of Applied Non-Classical Logics, 25(1):50-99, 2015. Google Scholar
  13. S. Demri, R. Fervari, and A. Mansutti. Axiomatising Logics with Separating Conjunction and Modalities. In JELIA'19, volume 11468 of LNAI, pages 692-708. Springer, 2019. Google Scholar
  14. S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. Separation Logic with One Quantified Variable. Theory of Computing Systems, 61:371-461, 2017. Google Scholar
  15. S. Demri, É. Lozes, and A. Mansutti. The Effects of Adding Reachability Predicates in Propositional Separation Logic. In FoSSaCS, volume 10803 of LNCS, pages 476-493. Springer, 2018. Google Scholar
  16. S. Demri, E. Lozes, and A. Mansutti. The Effects of Adding Reachability Predicates in Propositional Separation Logic. arXiv:1810.05410, October 2018. 44 pages. Long version of [S. Demri et al., 2018]. Google Scholar
  17. S. Demri, E. Lozes, and A. Mansutti. Internal Calculi for Separation logics. arXiv:1910.05016, October 2019. Google Scholar
  18. S. Docherty and D. Pym. Modular Tableaux Calculi for Separation Theories. In FoSSaCS'18, volume 10803 of LNCS, pages 441-458. Springer, 2018. Google Scholar
  19. A. Doumane. Constructive completeness for the linear-time μ-calculus. In LICS'17, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  20. M. Echenim, R. Iosif, and N. Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. In FoSSaCS'19, volume 11425 of LNCS, pages 242-259. Springer, 2019. Google Scholar
  21. D. Galmiche and D. Larchey-Wending. Expressivity properties of Boolean BI through relational models. In FST&TCS'06, volume 4337 of LNCS, pages 358-369. Springer, 2006. Google Scholar
  22. D. Galmiche and D. Méry. Tableaux and Resource Graphs for Separation Logic. Journal of Logic and Computation, 20(1):189-231, 2010. Google Scholar
  23. V. Goranko and G. van Drimmelen. Complete axiomatization and decidability of Alternating-time temporal logic. Theoretical Computer Science, 353(1-3):93-117, 2006. Google Scholar
  24. E. Grädel and I. Walukiewicz. Guarded Fixed Point Logic. In LICS'99, pages 45-54, 1999. Google Scholar
  25. Z. Hou, R. Clouston, R. Goré, and A. Tiu. Modular labelled sequent calculi for abstract separation logics. ACM Transactions on Computational Logic, 19(2):13:1-13:35, 2018. Google Scholar
  26. Z. Hou and A. Tiu. Completeness for a First-Order Abstract Separation Logic. In APLAS'16, volume 10017 of LNCS, pages 444-463. Springer, 2016. Google Scholar
  27. S. Ishtiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In POPL'01, pages 14-26. ACM, 2001. Google Scholar
  28. R. Kaivola. Axiomatising linear time mu-calculus. In CONCUR'95, volume 962 of LNCS, pages 423-437. Springer, 1995. Google Scholar
  29. E. Lozes. Expressivité des Logiques Spatiales. PhD thesis, ENS Lyon, 2004. Google Scholar
  30. E. Lozes. Separation Logic preserves the expressive power of classical logic. In SPACE'04, 2004. Google Scholar
  31. M. Lück. Axiomatizations of team logics. Annals of Pure and Applied Logic, 169(9):928-969, 2018. Google Scholar
  32. A. Mansutti. Extending Propositional Separation Logic for Robustness Properties. In FST&TCS'18, volume 122 of LIPIcs, pages 42:1-42:23. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  33. P.W. O'Hearn. A Primer on Separation Logic. In Software Safety and Security: Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series, pages 286-318, 2012. Google Scholar
  34. P.W. O'Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  35. R. Piskac, Th. Wies, and D. Zufferey. Automating Separation Logic using SMT. In CAV'13, volume 8044 of LNCS, pages 773-789. Springer, 2013. Google Scholar
  36. D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic. Kluwer Academic Publishers, 2002. Google Scholar
  37. D. Pym, J. Spring, and P.W. O'Hearn. Why Separation Logic Works. Philosophy & Technology, pages 1-34, 2018. Google Scholar
  38. J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55-74. IEEE, 2002. Google Scholar
  39. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157(1-2):142-182, 2000. Google Scholar
  40. Y. Wang and Q. Cao. On axiomatizations of public announcement logic. Synthese, 190(Supplement-1):103-134, 2013. Google Scholar
  41. H. Yang. Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign, 2001. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact