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 | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4141021