Transition Invariants

Proof rules for program verification rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invari-ants. A transition invariant of a program is a binary rela-tion over program states that contains the transitive closure of the transition relation of the program. A relation is dis-junctively well-founded if it is a finite union of well-founded relations. We characterize the validity of termination or an-other 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 ab-stract interpretation. 1