We present a complete method for synthesizing lexicographic linear ranking functions supported by inductive linear invariants for loops with linear guards and transitions. Proving termination via linear ranking functions often requires invariants; yet invariant generation is expensive. Thus, we describe a technique that discovers just the invariants necessary for proving termination. Finally, we describe an implementation of the method and provide extensive experimental evidence of its effectiveness for proving termination of C loops.
In Proc. of 17th International Conference on Computer Aided Verification (CAV'05), Springer Verlag, 2005, LNCS 3576, pp 491-504.
BibTex, Postscript, PDF, © 2005, Springer Verlag.