Reasoning on Dynamic Transformations of Symbolic Heaps - Laboratoire d'Informatique de Grenoble Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Reasoning on Dynamic Transformations of Symbolic Heaps

Résumé

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.
Fichier principal
Vignette du fichier
Peltier-TIME2022.pdf (818.05 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03844095 , version 1 (08-11-2022)

Identifiants

Citer

Nicolas Peltier. Reasoning on Dynamic Transformations of Symbolic Heaps. TIME 2022 : 29th International Symposium on Temporal Representation and Reasoning (TIME 2022), Nov 2022, online, France. ⟨10.4230/LIPIcs.TIME.2022.7⟩. ⟨hal-03844095⟩
10 Consultations
8 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More