Automating Program Proofs Based on Separation Logic with Inductive Definitions

Abstract. This paper investigates the use of Separation Logic with inductive definitions in reasoning about programs that manipulate dy-namic data structures. We propose a novel approach for exploiting the inductive definitions in automating program proofs based on inductive invariants. We focus on iterative programs, although our techniques ap-ply to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size. This approach is based on a careful inspection of the typical lem-mas needed in such program proofs and efficiently checkable criteria for recognizing inductive definitions that satisfy these lemmas. Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or delet-ing elements in binary search tress, red-black trees, and AVL trees, in a very efficient way.