Fast interpolating BMC

Yakir Vizel, Arie Gurfinkel, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

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

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 27th International Conference, CAV 2015, Proceedings
EditorsCorina S. Pasareanu, Daniel Kroening, Corina S. Pasareanu, Daniel Kroening
PublisherSpringer Verlag
Pages641-657
Number of pages17
ISBN (Print)9783319216898, 9783319216898
DOIs
StatePublished - Jan 1 2015
Event27th International Conference on Computer Aided Verification, CAV 2015 - San Francisco, United States
Duration: Jul 18 2015Jul 24 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9206
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other27th International Conference on Computer Aided Verification, CAV 2015
CountryUnited States
CitySan Francisco
Period7/18/157/24/15

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Fast interpolating BMC'. Together they form a unique fingerprint.

  • Cite this

    Vizel, Y., Gurfinkel, A., & Malik, S. (2015). Fast interpolating BMC. In C. S. Pasareanu, D. Kroening, C. S. Pasareanu, & D. Kroening (Eds.), Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings (pp. 641-657). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9206). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_43