A counterexample-guided interpolant generation algorithm for SAT-based model checking

Interpolation is an important and distinguished method popularly applied to recent synthesis and verification research topics. Existing approaches generate interpolants by analysing unsatisfiability proofs from SAT solvers. Unfortunately, the interpolant is predestinedly determined by how the unsatisfiability proof is logged. This particularly weakens the abstraction of interpolation-based model checking procedure. In this paper, a new approach to generate a variety of functionally different interpolants using simulation and SAT solving is proposed. We further seamlessly integrated the novel interpolant generation algorithm into the reinterpreted interpolation-based model checking procedure. Moreover, spurious counterexamples from the model checker further guide the generation of interpolants to refute excessive refinements. As an extra benefit, proof logging is not required for SAT solvers. Experiments show promising results of our interpolation-based model checker NewITP on solving a large set of HWMCC benchmarks.