License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2022.9
URN: urn:nbn:de:0030-drops-172566
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17256/
Peltier, Nicolas
Reasoning on Dynamic Transformations of Symbolic Heaps
Abstract
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.
BibTeX - Entry
@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/opus/volltexte/2022/17256},
URN = {urn:nbn:de:0030-drops-172566},
doi = {10.4230/LIPIcs.TIME.2022.9},
annote = {Keywords: Separation Logic, Symbolic Heaps, Linear Temporal Logic}
}
|
Keywords: |
|
Separation Logic, Symbolic Heaps, Linear Temporal Logic |
|
Collection: |
|
29th International Symposium on Temporal Representation and Reasoning (TIME 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
29.10.2022 |
