Jan Mikac and Paul Caspi
How many unfoldings of a program for proving an invariant? (2004)
How many unfoldings of a program for proving an invariant? (2004)
TR-2004-9.pdf
Keywords: induction, invariant, unfolding, abstraction
Abstract: This report proposes an improvement of automation for inductive proofs of invariant properties: a minimum number of unfoldings to perform a priori is proposed. The minimality comes from a characterisation of the pairs system--property where the property holds and can be proved by induction. Such a characterisation relies on several proof-conserving changes of variables. A real-world example of proof is given as an illustration.
