Interpolating Property Directed Reachability

摘要

Current SAT-based Model Checking is based on two major approaches: Interpolation-based (I_(MC)) (global, with unrollings) and Property Directed Reachability/IC3 (P_(DR)) (local, without unrollings). I_(MC) generates candidate invariants using interpolation over an unrolling of a system, without putting any restrictions on the SAT-solver's search. Pdr generates candidate invariants by a local search over a single instantiation of the transition relation, effectively guiding the SAT solver's search. The two techniques are considered to be orthogonal and have different strength and limitations. In this paper, we present a new technique, called A_(VY), that effectively combines the key insights of the two approaches. Like I_(MC), it uses unrollings and interpolants to construct an initial candidate invariant, and, like P_(DR), it uses local inductive generalization to keep the invariants in compact clausal form. On the one hand, A_(VY) is an incremental Imc extended with a local search for CNF interpolants. On the other, it is Pdr extended with a global search for bounded counterexamples. We implemented the technique using ABC and have evaluated it on the HWMCC benchmark-suite from 2012 and 2013. Our results show that the prototype significantly outperforms Pdr and McMillan's interpolation algorithm (as implemented in ABC) on the industrial sub-category of the benchmark.