Form Methods Syst Des DOI 10.1007/s10703-015-0224-5 Efficient generation of small interpolants in CNF

Abstract Interpolation-based model checking (ITP) McMillan (in CAV, 2003) is an efficient and complete model checking procedure. However, for large problems, interpolants gener-ated by ITP might become extremely large, rendering the procedure slow or even intractable. In this work we present a novel technique for interpolant generation in the context of model checking. The main novelty of our work is that we generate small interpolants in conjunctive normal form (CNF) using a twofold procedure: first we propose an algorithm that exploits resolution refutation properties to compute an interpolant approximation. Then we introduce an algorithm that takes advantage of inductive reasoning to turn the interpolant approxima-tion into an interpolant. Unlike ITP, our approach maintains only the relevant subset of the resolution refutation. In addition, the second part of the procedure exploits the properties of the model checking problem at hand, in contrast to the general-purpose algorithm used in ITP. We developed a new interpolation-based model checking algorithm, called CNF-ITP. Our algorithm takes advantage of the smaller interpolants and exploits the fact that the inter-polants are given in CNF. We integrated our method into a SAT-based model checker and experimented with a representative subset of the HWMCC’12 benchmark set. Our experi