Abstract
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. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Bradley, A. R., Manna, Z., & Sipma, H. B. (2005). Linear ranking with reachability. In Lecture Notes in Computer Science (Vol. 3576, pp. 491–504). Springer Verlag. https://doi.org/10.1007/11513988_48
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
