Linear Ranking with Reachability

Aaron R. Bradley, Zohar Manna, Henny Sipma

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.

© Henny Sipma /
Last modified: Wed Mar 28 16:10:48 PST 2001