Bounded Model Checking
References for ECEN 5139, Formal Verification of VLSI Systems
Class notes for BMC and SAT (in PDF),
Nov. 2003.
Related papers (pointing to the websites of the authors)
-
"Bounded
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.
-
"Chaff:
Engineering an Efficient SAT Solver," M.W. Moskewicz, C. Madigan, Y.
Zhao, L. Zhang and S. Malik. Proceedings of Design Automation Conference,
2001.
-
"GRASP:
A Search Algorithm for Satisfiability," J. P. M. Silva, K. A. Sakallah.
Technical
Report CSE-TR-292-96, The University of Michigan, 1996.
|