Abstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening
abstractions based on the analysis of these spurious counterexamples. For invariance properties, a counterexample is a finite
trace that violates the invariant; it is spurious if it is possible in the abstraction but not in the original system. When
proving termination or other liveness properties of infinite-state systems, a useful notion of spurious counterexamples has
remained an open problem. For this reason, no counterexample-guided abstraction refinement algorithm was known for termination.
In this paper, we address this problem and present the first known automatic counterexample-guided abstraction refinement
algorithm for termination proofs. We exploit recent results on transition invariants and transition predicate abstraction.
We identify two reasons for spuriousness: abstractions that are too coarse, and candidate transition invariants that are too
strong. Our counterexample-guided abstraction refinement algorithm successively weakens candidate transition invariants and
refines the abstraction.