Bounded Model Checking

Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu. Symbolic Model Checking without BDDs.
In Proc. Intl. Conf. on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99),
Lecture Notes in Computer Science (LNCS), vol. 1579, Springer 1999.

The BMC page at CMU contains the original implementation and benchmarks.

Here are copies of the latest available version of the code bmc-1-0-f.tar.gz (July 14, 1999) and the generated CNF benchmarks BMC-dimacs-examples-0.0.tar.gz.

CAV 2018 Award

At CAV 2018 in Oxford, UK, we received for our work on bounded model checking for Hardware (BMC) the prestigious CAV Award jointly with Daniel Kroening and Flavio Lerda for their extension to Software (CBMC), also together with Edmund Clarke.

The slides of the award talk are available here: Biere-CAV18Award-talk.pdf.

The official quote for the award is as follows. For their outstanding contribution to the enhancement and scalability of model checking by introducing Bounded Model Checking based on Boolean Satisfiability (SAT) for hardware (BMC) and software (CBMC).

The full award nominations is available at the CAV 2018 Award page. A local copy is avaiable too.

ETAPS 2017 Test of Time Award

At ETAPS'17 in Uppsala we received for this paper the ETAPS'17 Test of Time Award.

The nomination from the official ETAPS 2017 Test of Time Award site (local copy) says that our paper made two fundamental contributions to model checking and automated verification:

The first involves the use of general-purpose SAT solvers to replace specialized decision procedures based on Boolean Decision Diagrams (BDDs) during the model-checking process ...

The second fundamental contribution of the paper is the invention of the so-called bounded model checking technique for system verification. ... This paper instead advocated the idea that the purpose of model checking was to detect bugs, ...

Most Influential in the first 20 years of TACAS

At TACAS'14 in Grenoble we received for this paper the award for most influential paper in the first 20 years of TACAS.

Also described in the 5th issue of the ETAPS'14 daily.