Sciweavers

CAV
2005
Springer
135views Hardware» more  CAV 2005»
14 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 ...
Aaron R. Bradley, Zohar Manna, Henny B. Sipma