Bounded Model Checking
References for ECEN 5139, Formal Verification of VLSI Systems
Class notes for BMC and SAT (in PDF),
Related papers (pointing to the websites of the authors)
Model Checking," A. Biere, A. Cimatti, E. M. Clarke, O. Strichman and
Y. Zhu. Vol. 58 of Advances in Computers, 2003. Academic Press (pre-print)
"Checking safety properties
using induction and a SAT-solver," M. Sheeran, S. Singh and G. Stalmarck,
Formal methords in Computer Aided Design, 2000.
Engineering an Efficient SAT Solver," M.W. Moskewicz, C. Madigan, Y.
Zhao, L. Zhang and S. Malik. Proceedings of Design Automation Conference,
A Search Algorithm for Satisfiability," J. P. M. Silva, K. A. Sakallah.
Report CSE-TR-292-96, The University of Michigan, 1996.