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.
For this paper we received at TACAS'14 in
Grenoble the award for most influential paper in the first 20 years
Also described in the
5th issue of the ETAPS'14