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.

For this paper we received at TACAS'14 in Grenoble 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.