Proving Data Structure Properties by Automatic Induction

We consider the problem of automated program verification with emphasis on reasoning about dynamically manipulated data struc-tures. Presently, the state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm where predicates are trans-formed by fold/unfold operations induced from their recursive def-initions. A crucial limitation of U+M is that it cannot in general prove properties between different predicates. Our contribution is a method which can automatically detect and employ induction hypothesis in the proof process, thereby providing a systematic and general method for reasoning about different predicates for the first time. After arguing that the need for this is in fact widespread in practice, we finally demonstrate our method experimentally. 1