Fast Interpolating Bounded Model Checking

Опубликовано 27 июня 2016, 21:23

Bounded 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.