Interpolation-based model checking (IMC) is an important technique in modern formal verification tools. In essence, it relies on an abstraction and refinement process to derive an adequate image approximation for the reachability analysis. However, previous IMC algorithms only offer fixed degrees of abstraction and thus may fail in the proofs if the abstraction is too coarse- or fine-grained. In this paper, we propose an adaptive interpolation-based model checking algorithm in which the degree of abstraction can be adjusted on demand. That is, during the proof process, we closely monitor the effectiveness of the interpolation-based over-approximated image computation and thus adjust the degree of abstraction for the best performance. The experimental results confirm that our flexible interpolation indeed leads to an adequate degree of abstraction as our IMC algorithm outperforms previous ones in various aspects.

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.

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.

In this paper, we propose a property-specific sequential invariant extraction algorithm to improve the performance of the SAT-based Unbounded Modeling Checkers (UMCs). By analyzing the property-related predicates and their corresponding high-level design constructs such as FSMs and counters, we can quickly identify the sequential invariants that are useful in improving the property proving capabilities. We utilize these sequential invariants to refine the inductive hypothesis in induction-based UMCs, and to improve the accuracy of reachable state approximation in interpolation-based UMCs. The experimental results show that our tool can outperform a state-of-the-art UMC in most cases, especially for the difficult true properties.