Fast interpolating BMC

7Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

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.

References Powered by Scopus

An extensible SAT-solver

1846Citations
N/AReaders
Get full text

Symbolic model checking without BDDs

1595Citations
N/AReaders
Get full text

Bounded Model Checking

694Citations
N/AReaders
Get full text

Cited by Powered by Scopus

Accelerating syntax-guided invariant synthesis

28Citations
N/AReaders
Get full text

Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing

9Citations
N/AReaders
Get full text

Function summarization modulo theories

6Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

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

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 5

100%

Readers' Discipline

Tooltip

Engineering 3

60%

Computer Science 2

40%

Save time finding and organizing research with Mendeley

Sign up for free