Approximation Refinement for Interpolation-Based Model Checking

Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from the SAT solver to progress. If an over-approximation leads to a satisfiable formula, the computation restarts using more constraints and the previously computed approximation is not reused. Though the new formula eliminates spurious counterexamples of a certain length, there is no guarantee that the subsequent approximation is better than the one previously computed. We take an abstract, approximation-oriented view of interpolation based model checking. We study counterexample-free approximations, which are neither over- nor under-approximations of the set of reachable states but still contain enough information to conclude if counterexamples exist. Using such approximations, we devise a model checking algorithm for approximation refinement and discuss a preliminary implementation of this technique on some hardware benchmarks.