[ etaps-2017-test-of-time-award |
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.
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 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