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.

• Type: Conference
• Year: 2005
• Where: CAV
• Authors: Aaron R. Bradley, Zohar Manna, Henny B. Sipma
• Keywords: CAV 2005, Formal Methods, Inductive Linear Invariants, Lexicographic Linear, Linear Ranking Functions