Linear Ranking with Reachability

10 years 1 months ago
Linear Ranking with Reachability
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.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Aaron R. Bradley, Zohar Manna, Henny B. Sipma
Comments (0)