Bounded Model Checking

A. Biere, A. Cimatti, E. Clarke, Y. 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.

ETAPS 2017 Test of Time Award

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

ETAPS 2017 Award 1 ETAPS 2017 Award 2
ETAPS 2017 Award 1 ETAPS 2017 Award 2

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.

Award Certificate fo Most Influential Paper in the first 20 Years of TACAS Award Celebration Picture for Most Influential Paper in the first 20 Years of TACAS

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