Internal Calculi for Separation Logics
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.
Separation logic
internal calculus
adjunct/quantifier elimination
Theory of computation
19:1-19:18
Regular Paper
We would like to thank the anonymous reviewers for their suggestions and remarks that help us to improve the quality of this paper.
Stéphane
Demri
Stéphane Demri
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
Etienne
Lozes
Etienne Lozes
Université Côte d’Azur, CNRS, I3S, France
Alessio
Mansutti
Alessio Mansutti
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
10.4230/LIPIcs.CSL.2020.19
C. Areces, P. Blackburn, and M. Marx. Hybrid logics: characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3):977-1010, 2001.
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.
M. Bozga, R. Iosif, and S. Perarnau. Quantitative Separation Logic and Programs with Lists. Journal of Automated Reasoning, 45(2):131-156, 2010.
R. Brochenin, S. Demri, and E. Lozes. On the Almighty Wand. Information and Computation, 211:106-137, 2012.
J. Brotherston. Bunched Logics Displayed. Studia Logica, 100(6):1223-1254, 2012. URL: https://doi.org/10.1007/s11225-012-9449-0.
https://doi.org/10.1007/s11225-012-9449-0
J. Brotherston and M. Kanovich. Undecidability of Propositional Separation Logic and Its Neighbours. Journal of the Association for Computing Machinery, 61(2), 2014.
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.
J. Brotherston and J. Villard. Parametric completeness for separation theories. In POPL'14, pages 453-464. ACM, 2014.
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.
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.
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.
S. Demri and M. Deters. Separation Logics and Modalities: A Survey. Journal of Applied Non-Classical Logics, 25(1):50-99, 2015.
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.
S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. Separation Logic with One Quantified Variable. Theory of Computing Systems, 61:371-461, 2017.
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.
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].
S. Demri, E. Lozes, and A. Mansutti. Internal Calculi for Separation logics. arXiv:1910.05016, October 2019.
S. Docherty and D. Pym. Modular Tableaux Calculi for Separation Theories. In FoSSaCS'18, volume 10803 of LNCS, pages 441-458. Springer, 2018.
A. Doumane. Constructive completeness for the linear-time μ-calculus. In LICS'17, pages 1-12. IEEE Computer Society, 2017.
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.
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.
D. Galmiche and D. Méry. Tableaux and Resource Graphs for Separation Logic. Journal of Logic and Computation, 20(1):189-231, 2010.
V. Goranko and G. van Drimmelen. Complete axiomatization and decidability of Alternating-time temporal logic. Theoretical Computer Science, 353(1-3):93-117, 2006.
E. Grädel and I. Walukiewicz. Guarded Fixed Point Logic. In LICS'99, pages 45-54, 1999.
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.
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.
S. Ishtiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In POPL'01, pages 14-26. ACM, 2001.
R. Kaivola. Axiomatising linear time mu-calculus. In CONCUR'95, volume 962 of LNCS, pages 423-437. Springer, 1995.
E. Lozes. Expressivité des Logiques Spatiales. PhD thesis, ENS Lyon, 2004.
E. Lozes. Separation Logic preserves the expressive power of classical logic. In SPACE'04, 2004.
M. Lück. Axiomatizations of team logics. Annals of Pure and Applied Logic, 169(9):928-969, 2018.
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.
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.
P.W. O'Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999.
R. Piskac, Th. Wies, and D. Zufferey. Automating Separation Logic using SMT. In CAV'13, volume 8044 of LNCS, pages 773-789. Springer, 2013.
D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic. Kluwer Academic Publishers, 2002.
D. Pym, J. Spring, and P.W. O'Hearn. Why Separation Logic Works. Philosophy & Technology, pages 1-34, 2018.
J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55-74. IEEE, 2002.
I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157(1-2):142-182, 2000.
Y. Wang and Q. Cao. On axiomatizations of public announcement logic. Synthese, 190(Supplement-1):103-134, 2013.
H. Yang. Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign, 2001.
Stéphane Demri, Etienne Lozes, and Alessio Mansutti
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode