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 paper, we present a Fast Interpolating BMC (Fib) that combines state-of-the-art BMC techniques with interpolation. We show how to interpolate in the presence of circuit-aware simplifications and in the context of incremental solving. We evaluate our implementation of Fib in AVY, an interpolating property directed model checker, and show that it has a great positive effect on the overall performance. With the Fib, AVY outperforms ABC implementation of Pdr on both HWMCC’13 and HWMCC’14 benchmarks.
Mendeley helps you to discover research relevant for your work.
CITATION STYLE
Vizel, Y., Gurfinkel, A., & Malik, S. (2015). Fast interpolating BMC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9206, pp. 641–657). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_43