Labelled sequent calculi and automated reasoning for assertions in separation logic

Abstract

Separation logic (SL) is an extension of Hoare logic to reason about programs with mutable data structures. This thesis studies automated reasoning for the assertional language (i.e., formulae that represent pre- and post-conditions) of separation logic. We start from the core of separation logic called Boolean BI (BBI), then consider various propositional abstract separation logics (PASLs) as extensions of BBI. These logics are "abstract" because they are independent of any particular concrete memory model. Finally, we look at separation logic with Reynolds's heap model semantics. We first try to capture BI logics using nested sequents, our design has a special structure of interleaving additive and multiplicative nested sequents. We discover that this nested structure causes much complication when considering the rules for transferring information between nested sequents. Then we change the angle to solve this problem by using labelled sequents. We present a labelled sequent calculus LS_BBI for BBI, the calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in LS_BBI can be localised around applications of certain logical rules, based on which we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Based on LS_BBI, we develop a modular proof theory for various PASLs using cut-free labelled sequent calculi. We first extend LS BBI to handle Calcagno et al.'s original logic of separation algebras by adding rules for partial-determinism and cancellativity. We prove the completeness of our calculus via an intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other PASLs by adding rules for other properties in separation theory. We present a theorem prover based on our labelled calculi for these logics. For concrete heap semantics, we consider Reynolds's SL with all logical connectives but without arbitrary predicates. This logic is not recursively enumerable but is very useful in practice. We give a sound labelled sequent calculus LS_SL for this logic. We illustrate the subtle deficiencies of some existing proof calculi for SL, and show that our rules repair these problems. We extend LS SL with rules for linked lists and binary trees, giving a sound, complete and terminating proof system for a popular fragment called symbolic heaps. Our prover shows comparable results with Smallfoot on valid formulae and on formulae extracted from program verification examples, but it is not competitive on large invalid formulae. However, our prover handles the largest fragment of logical connectives in SL. Show more