Fast Interpolating Bounded Model Checking

  • Yakir Vizel | Princeton University

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.

Speaker Details

Yakir Vizel is presently a postdoctoral research associate at Princeton University working under the supervision of Professor Sharad Malik. He received his PhD from The Technion in Israel. He worked in the EDA industry for 10 years developing model checking and formal verification solutions. His research interests include model checking, abstraction, satisfiability solving and interpolation.

    • Portrait of Jeff Running

      Jeff Running

Series: Microsoft Research Talks