Labelled Cyclic Proofs for Separation Logic - Université de Lorraine
Article Dans Une Revue Journal of Logic and Computation Année : 2021

Labelled Cyclic Proofs for Separation Logic

Didier Galmiche
Daniel Mery

Résumé

Separation Logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. It is successful for program verification as an assertion language to state properties about memory heaps using Hoare triples. Most of the proof systems and verification tools for SL focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof systems that go beyond symbolic heaps are purely syntactic or labelled systems dedicated to some fragments of SL and they mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. In this work, we present a labelled proof system, called GMSL, that allows both the definition of cyclic proofs with arbitrary inductive predicates and the full set of SL connectives. We prove its soundness and show that we can derive in GMSL the built-in rules for data structures of another non-cyclic labelled proof system and also that GMSL is strictly more powerful than that system.
Fichier non déposé

Dates et versions

hal-03563631 , version 1 (09-02-2022)

Identifiants

Citer

Didier Galmiche, Daniel Mery. Labelled Cyclic Proofs for Separation Logic. Journal of Logic and Computation, 2021, 31 (3), pp.892-922. ⟨10.1093/logcom/exab017⟩. ⟨hal-03563631⟩
36 Consultations
0 Téléchargements

Altmetric

Partager

More