Labelled Cyclic Proofs for Separation Logic
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.