Accelerating Interpolants ⋆
2013
Abstract. We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR),anew algorithm for verifyinginfinite-state transitionsystems. CEGAARcombines interpolation-basedpredicate discovery incounterexampleguided predicate abstraction withacceleration technique for computing the transitiveclosure of loops.CEGAARappliesaccelerationtodynamicallydiscovered 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. Wepresent theoretical andexperimental justificationforthe effectiveness ofCE-GAAR,showingthatinductiveinterpolantscanbecomputedfromclassicalCraig interpolants and transitive closures of loops. We present an implementation of CEGAARthat verifiesinteger transitionsystems. We show that the resultingimplementationrobustlyhandlesanumberofdifficulttransitionsystemsthatcannot be handled usinginterpolation-based predicate abstraction or acceleration alone. 1