HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Labelled Cyclic Proofs for Separation Logic

Didier Galmiche 1 Daniel Mery 1
1 TYPES - Logic, Proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Journal articles
Complete list of metadata

https://hal.univ-lorraine.fr/hal-03563631
Contributor : Didier Galmiche Connect in order to contact the contributor
Submitted on : Wednesday, February 9, 2022 - 7:16:18 PM
Last modification on : Friday, April 1, 2022 - 3:44:41 AM

Identifiers

  • HAL Id : hal-03563631, version 1

Collections

Citation

Didier Galmiche, Daniel Mery. Labelled Cyclic Proofs for Separation Logic. Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.892-922. ⟨hal-03563631⟩

Share

Metrics

Record views

12