Pointers and sharing have always been difficult problems in program verification, and several extensions to Hoare logic have been proposed and investigated over the decades.

A very promising, quite recent approach is Reynolds’ separation logic, which draws on experiences in substructural or resource-sensitive logics having connectives different from classical logic.

This paper is concerned with proof search in the propositional kernel of abstract separation logics (PASL), which have algebraic structures as models that abstract away the details of a concrete memory model. These abstract separation logics are in several ways similar to the logic of Boolean bunched implications (BBI).

The paper starts with a short introduction that gives a historical perspective and raises the question of whether the proof theory developed for BBI can be useful for PASL. Following this, a labeled sequent calculus for PASL is derived, and it is shown that the cut-elimination property of the labeled sequent calculus for BBI easily transfers to PASL.

The next section presents a Kripke-style semantics for PASL and a corresponding completeness proof. Extensions of the sequent calculus with rules that have already been proposed for some variant separation logics are the focus of the next two sections, and it is shown that some of the extensions are compatible with the results proved in the previous sections and some are not. An implementation of proof search in the sequent calculus for PASL with the addition of the disjointness rule is considered in the following section, and the results of several experimental proof searches are stated. The paper concludes with two sections on future and related work.

While this paper is very interesting for researchers working in program verification, it cannot be read in isolation because the necessary basic intuitions stemming from programming are not provided. Reynolds’ seminal paper on separation logic [1] should be read first. From a purely logical perspective, it is mainly self-contained, only referencing several proofs as being analogous to already-published proofs.