Proof automation for functional correctness in separation logic

Abstract

We describe an approach to automatically verify goals stated in substructural logics. In particular we are interested in proving the functional correctness of pointer programs that involve iteration and recursion. Building upon separation logic, our approach has been implemented as a tightly integrated tool chain – where a novel combination of proof planning and invariant generation lies at its core. Starting from shape analysis, performed by the Smallfoot static analyser, we have developed a proof strategy that combines shape and functional aspects of the verification task. By focusing on both iterative and recursive code, we have had to address two related invariant generation tasks, i.e. loop and frame invariants. We deal with both tasks uniformly using an automatic technique called term synthesis, in combination with the IsaPlanner/Isabelle theorem prover. In addition, where verification fails, we attempt to overcome failure by automatically generating missing preconditions. We present in detail our experimental results. Our approach has been evaluated on a range of examples, drawn in part from a functional extension to the Smallfoot corpus. While our focus is the functional correctness of pointer programs, our proof techniques are applicable to substructural logics in general, but in particular linear logic [12] and the logic of bunched implications [27].