Verimag

Technical Reports

Jan Mikac and Paul Caspi
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.

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 791452