Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Labelled Cyclic Proofs for Separation Logic

Didier Galmiche 1 Daniel Méry 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. SL has proven itself successful in the field of program verification over the past fifteen years as an assertion language to state properties about memory heaps using Hoare triples. Since the full logic is not recursively enumerable, 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 allow either the full set of connectives, or the definition of arbitrary predicates, but not both. In this work, we present a labelled proof-system, called GMSL, that allows both the definition of arbitrary inductive predicates and the full set of SL connectives.
Document type :
Conference papers
Complete list of metadata
Contributor : Didier GALMICHE Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2020 - 4:47:05 PM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM


  • HAL Id : hal-02982617, version 1



Didier Galmiche, Daniel Méry. Labelled Cyclic Proofs for Separation Logic. International Workshop on Automated Deduction for Separation Logics, ADSL 2018, 2018, Oxford, United Kingdom. ⟨hal-02982617⟩



Record views