Sciweavers

CAV
2015
Springer

Fast Interpolating BMC

8 years 6 months ago
Fast Interpolating BMC
Abstract. 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 ...
Yakir Vizel, Arie Gurfinkel, Sharad Malik
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CAV
Authors Yakir Vizel, Arie Gurfinkel, Sharad Malik
Comments (0)