[ cav-2018-award | etaps-2017-test-of-time-award |
Bounded Model Checking
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu.
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.
page at CMU contains the original implementation and
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.
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.
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
The full award nominations is available at the CAV 2018 Award page.
A local copy is avaiable too.
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, ...
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