Proof tactics for assertions in separation logic

Abstract

This paper presents tactics for reasoning about the assertions of separation logic. We formalise our proof methods in Isabelle/HOL based on Klein et al.’s separation algebra library. Our methods can also be used in other separation logic frameworks that are instances of the separation algebra of Calcagno et al. The first method, separata, is based on an embedding of a labelled sequent calculus for abstract separation logic (ASL) by Hóu et al. The second method, starforce, is a refinement of separata with specialised proof search strategies to deal with separating conjunction and magic wand. We also extend our tactics to handle pointers in the heap model, giving a third method sepointer. Our tactics can automatically prove many complex formulae. Finally, we give two case studies on the application of our tactics.