We present Counterexample-Guided Accelerated Abstraction Refinement
(CEGAAR), a new algorithm for verifying infinite-state transition
systems.  CEGAAR combines interpolation-based predicate discovery in
counterexample-guided predicate abstraction with acceleration
technique for computing the transitive closure of loops. CEGAAR
applies acceleration to dynamically discovered looping patterns in the
unfolding of the transition system, and combines overapproximation
with underapproximation. It constructs inductive invariants that rule
out an infinite family of spurious counterexamples, alleviating the
problem of divergence in predicate abstraction without losing its
adaptive nature. We present theoretical and experimental justification
for the effectiveness of CEGAAR, showing that inductive interpolants
can be computed from classical Craig interpolants and transitive
closures of loops. We present an implementation of CEGAAR that
verifies integer transition systems. We show that the resulting
implementation robustly handles a number of difficult transition
systems that cannot be handled using interpolation-based predicate
abstraction or acceleration alone.