Completeness for a First-order Abstract Separation Logic

TL;DR

This paper introduces FOASL, a first-order separation logic with an abstracted points-to predicate, providing a sound and complete framework for reasoning about program verification with concrete and non-standard semantics.

Contribution

It develops FOASL, a novel first-order separation logic with an abstracted points-to predicate, and proves its soundness and completeness relative to an abstract semantics.

Findings

FOASL is sound and complete for an abstract semantics.

The logic can approximate reasoning principles involving the points-to predicate.

The theorem prover handles a large fragment of separation logic with various semantics.

Abstract

Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is not possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynolds's semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.