Proving Data Structure Properties by Automatic Induction
Duc-Hiep Chu, Joxan Jaffar, Minh-Thai Trinh · 2013
Abstract. We consider the problem of automated program verification with emphasis on reasoning about dynamically manipulated data struc-tures. Presently, in handling user-defined recursive predicates, the state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm where predicates are transformed by fold/unfold operations induced from their definitions. A crucial limitation of U+M is that it cannot in gen-eral 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 argu-ing that the need for this is in fact widespread in practice, we finally demonstrate our method experimentally. 1