Labelled Cyclic Proofs for Separation Logic - Archive ouverte HAL Access content directly
Journal Articles Journal of Logic and Computation Year : 2021

Labelled Cyclic Proofs for Separation Logic

Didier Galmiche
Daniel Mery

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.
Not file

Dates and versions

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

Identifiers

  • HAL Id : hal-03563631 , version 1

Cite

Didier Galmiche, Daniel Mery. Labelled Cyclic Proofs for Separation Logic. Journal of Logic and Computation, 2021, 31 (3), pp.892-922. ⟨hal-03563631⟩
16 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More