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.
@InProceedings{peltier:LIPIcs.TIME.2022.9, author = {Peltier, Nicolas}, title = {{Reasoning on Dynamic Transformations of Symbolic Heaps}}, booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)}, pages = {9:1--9:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-262-4}, ISSN = {1868-8969}, year = {2022}, volume = {247}, editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.9}, URN = {urn:nbn:de:0030-drops-172566}, doi = {10.4230/LIPIcs.TIME.2022.9}, annote = {Keywords: Separation Logic, Symbolic Heaps, Linear Temporal Logic} }
Feedback for Dagstuhl Publishing