eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-10-29
9:1
9:20
10.4230/LIPIcs.TIME.2022.9
article
Reasoning on Dynamic Transformations of Symbolic Heaps
Peltier, Nicolas
1
Univ. Grenoble Alpes, CNRS, LIG, Grenoble, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol247-time2022/LIPIcs.TIME.2022.9/LIPIcs.TIME.2022.9.pdf
Separation Logic
Symbolic Heaps
Linear Temporal Logic