Abstraction Refinement for Termination

ion can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strength- ening abstractions based on the analysis of these spurious counterex- amples. 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 coun- terexamples has remained an open problem. No counterexample-guided abstraction refinement algorithm was known for termination. In this pa- per, 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: abstrac- tions 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 ab- straction.