Lilia Georgieva, Patrick Maier Inductive Reasoning for Shape Invariants ABSTRACT: Automatic verification of imperative programs that destructively manipulate 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 solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications. KEYWORDS: program verification, application of first-order theorem provers, logic programs.