Abstract:

Proving termination of an infinite-state loop is traditionally
accomplished through the ranking function method.  In this method, a
proposed ranking function and the loop generate a set of verification
conditions.  If each of these verification conditions is proved
loop-valid (i.e., true at all reachable states of the loop), then the
loop always terminates.  In the first part of the talk, we focus on
formally defining these concepts and showing applications to several
interesting loops.

In practice, we desire automated discovery and proof of termination.
We next present a method for the synthesis of ranking functions on
linear loops.  Specifically, the method synthesizes a linear
lexicographic ranking function for a linear loop, supported by a
linear invariant, if one exists.  The supporting invariant transforms
loop validity into first-order validity.  We present experimental
evidence indicating that synthesis is a powerful technique for scaling
deductive verification to large programs.