Transition invariants

TLDR

Proof rules for program verification rely on auxiliary assertions, and a transition invariant is a binary relation over program states that includes the transitive closure of the program’s transition relation, with such relations being disjunctively well-founded when they are finite unions of well-founded relations. The authors propose a sound and relatively complete proof rule that uses transition invariants as auxiliary assertions. The rule characterizes termination or liveness by requiring a disjunctively well‑founded transition invariant, and the authors propose a sound and relatively complete proof rule that uses such invariants as auxiliary assertions. The proof rule’s main contribution is its potential for automation through abstract interpretation.

Abstract

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.