2026-07-23T22:34:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17256 2024-03-06T10:59:20Z ddc:004 open_access

Reasoning on Dynamic Transformations of Symbolic Heaps Peltier, Nicolas Separation Logic Symbolic Heaps Linear Temporal Logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nicolas Peltier 2022 Is Part Of LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2022.9 urn:nbn:de:0030-drops-172566 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.9 eng https://creativecommons.org/licenses/by/4.0/legalcode