Automated theorem proving for assertions in separation logic with all connectives

Abstract

This paper considers Reynolds’s separation logic 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 for this logic. Using numerous examples, we illustrate the subtle deficiencies of several existing proof calculi for separation logic, and show that our rules repair these deficiencies. We extend the calculus 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 has comparable performance to Smallfoot, a prover dedicated to symbolic heaps, on valid formulae extracted from program verification examples; but our prover is not competitive on invalid formulae. We also show the ability of our prover beyond symbolic heaps, our prover handles the largest fragment of logical connectives in separation logic.