Automatic induction proofs of data-structures in imperative programs

8 years 6 months ago

Download www.comp.nus.edu.sg

We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose deﬁnitions are formalized via user-deﬁned recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we ﬁnd a sequence of transformations that produces a ﬁnal formula which is obviously provable by simply matching terms. Our contribution here is the addition of the fundamental principle of induction to this automated process. We ﬁrst show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained by using the fold/unfold operations. While the adding of inducti...

Duc-Hiep Chu, Joxan Jaffar, Minh-Thai Trinh

Real-time Traffic