[ cav-2018-award | etaps-2017-test-of-time-award | tacas-most-influential-paper-award ]
Bounded Model Checking
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu.
Model Checking without BDDs.
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.
CAV 2018 Award
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.
The full award nominations is available at the CAV 2018 Award page. A local copy is avaiable too.
ETAPS 2017 Test of Time Award
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:
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.
Also described in the 5th issue of the ETAPS'14 daily.