Logic in Computer Science, Symposium on (2004)
July 13, 2004 to July 17, 2004
Andreas Podelski , Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany
Andrey Rybalchenko , Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany
Proof rules for program verification rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invariants. A transition invariant of a program is a binary relation over program states that contains the transitive closure of the transition relation of the program. A relation is disjunctively well-founded if it is a finite union of well-founded relations. We characterize the validity of termination or another liveness property by the existence of a disjunctively well-founded transition invariant. The main contribution of our proof rule lies in its potential for automation via abstract interpretation.
Andreas Podelski, Andrey Rybalchenko, "Transition Invariants", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 32-41, 2004, doi:10.1109/LICS.2004.1319598