Inductive Reasoning for Shape Invariants

Automatic verification of imperative programs that destructively ma- nipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solu- tions of logic programs. We use off-the-shelffirst-order theorem provers to reason about these specifications.