Separation Logic + Superposition Calculus = Heap Theorem Prover

Program analysis crucially depends on the ability to symbolically describe and reason about sets of program behaviours. Separation logic provides a promising foundation for dealing with heap manipulating programs, but the development of efficient inference tools for separation logic remains a challenging problem. In this talk I will present my work on designing an efficient, sound and complete automated theorem prover for checking the validity of entailments in a fragment of separation logic with list segment predicates. Our prover is built from a modular integration of separation logic techniques---to reason about the shape of structures in memory---and superposition calculus---to reason about equality/aliasing between memory locations. I will also present some empirical evaluation of the efficiency of this procedure, which indicates speedups of several orders of magnitude with respect to previous techniques, and discuss possible generalisations of this procedure to deal with other inductive predicates (e.g. trees) and in conjunction with other theories (e.g. arithmetic).