Reasoning on Dynamic Transformations of Symbolic Heaps
Building on previous results concerning the decidability of the satisfiability and entailment problems for separation logic formulas with inductively defined predicates, we devise a proof procedure to reason on dynamic transformations of memory heaps. The initial state of the system is described by a separation logic formula of some particular form, its evolution is modeled by a finite transition system and the expected property is given as a linear temporal logic formula built over assertions in separation logic.
Separation Logic
Symbolic Heaps
Linear Temporal Logic
Theory of computation~Separation logic
Theory of computation~Automated reasoning
Theory of computation~Modal and temporal logics
9:1-9:20
Regular Paper
This work has been partially funded by the the French National Research Agency (ANR-21-CE48-0011).
Nicolas
Peltier
Nicolas Peltier
Univ. Grenoble Alpes, CNRS, LIG, Grenoble, France
10.4230/LIPIcs.TIME.2022.9
Callum Bannister, Peter Höfner, and Gerwin Klein. Backwards and forwards with separation logic. In Jeremy Avigad and Assia Mahboubi, editors, ITP 2018, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of LNCS, pages 68-87. Springer, 2018.
Rémi Brochenin, Stéphane Demri, and Étienne Lozes. Reasoning about sequences of memory states. In Sergei N. Artëmov and Anil Nerode, editors, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, volume 4514 of LNCS, pages 100-114. Springer, 2007.
James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 25:1-25:10. ACM, 2014.
Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In LPAR 2020, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 191-211. EasyChair, 2020.
Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In CSL 2021, EPiC Series in Computing. EasyChair, 2021.
Didier Galmiche and Daniel Méry. Labelled tableaux for linear time bunched implication logic. In ASL 2022 (Workshop on Advancing Separation Logic), 2022.
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.
Norihiro Kamide. Temporal BI: proof system, semantics and translations. Theor. Comput. Sci., 492:40-69, 2013.
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM, 53(6):937-977, 2006.
Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bull. Symb. Log., 5(2):215-244, 1999.
Jens Pagel, Christoph Matheja, and Florian Zuleger. Complete entailment checking for separation logic with inductive definitions, 2020. URL: http://arxiv.org/abs/2002.01202.
http://arxiv.org/abs/2002.01202
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.
Amir Pnueli. The temporal logic of programs. In FOCS, Providence, Rhode Island, USA, pages 46-57. IEEE Computer Society, 1977.
J.C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS'02, 2002.
Nicolas Peltier
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode