Fast Interpolating Bounded Model Checking
6Bounded Model Checking (BMC) is well known for its simplicity and ability to find counterexamples. It is based on the idea of symbolically representing counterexamples in a transition system and then using a SAT-solver to check for their existence or their absence. State-of-the-art BMC algorithms combine a direct translation to SAT with circuit-aware simplifications and work incrementally, sharing information between different bounds. While BMC is incomplete (it can only show existence of counterexamples), it is a major building block of several complete interpolation-based model checking algorithms. However, traditional interpolation is incompatible with optimized BMC. Hence, these algorithms rely on simple BMC engines that significantly hinder their performance. In this talk, we present a Fast Interpolating BMC (FIB) engine that combines state-of-the-art BMC techniques with interpolation. We show how to interpolate in the presence of circuit-aware simplifications. In addition, we discuss incremental DRUP-proof logging needed for interpolation. We conclude by presenting results of our evaluation of FIB in AVY, an interpolating property directed model checker, and show that it has a great positive effect on the overall performance.