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 analyzing unsatisfiability (UNSAT) proofs from satisfiable (SAT) solvers. Unfortunately, the interpolant is predestinedly determined by how the UNSAT 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 a 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.