Litreature Survey report on Bounded Model Checking

Related Papers 
[ABZ99] Edmund Clarke Armin Biere, Alessandro Cimatti
and Yunshan Zhu.  Symbolic model checking without
bdds. In TACAS, 1999.

[BCM+90] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill,
and L. G.  Hwang. Symbolic model checking 10exp20 states and beyond. In Logic
in Computer Science, pages 428-439, 1990.

[BCRZ99] A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying
safety properties of a powerpc microprocessor using symbolic model checking
without bdds. In Lecture Notes in Computer Science, pages 60-71,
1999.

[Bry86] R. E. Bryant. Graph based algorithm for boolean function
manip

ulation. In IEEE Transaction on Computers, 1986.

[CBL+94] E. M. Clarke, J. R. Burch, D. E. Long, K. L. McMillan, 
and D. L.  Dill. Symbolic model checking for sequential circuit 
verification. In IEEE Transaction on Computer Aided Design of Integrated
Circuits and Systems, pages 401-424, 1994.

[DP60] M. Davis and H. Putnam. A computing procedure for
quantification

theory. In Journal of the Association for Computing Machinery,
pages 201-215, 1960.

[EMCP99]Book Available in CFDVS library
Orna Grumberg Edmund M. Clarke, Jr. and Doron A. Peled.  Model
Checking. Cambridge, MA, 1999.

[EOK94] E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look 
at LTL model checking. In David L. Dill, editor, Proceedings of
the sixth International Conference on Computer-Aided Verification
CAV, volume 818, pages 415-427, Standford, California, USA, 1994.
Springer-Verlag.

[FCV00] Ranan Fraer, Enrico Giunchiglia,
Gila Kamhi, Armando Tacchella Fady Copty, Limor Fix
and Moshe Y. Vardi. Benifits of bounded
model checking at an industrial setting. In CAV, pages 436-453,
2001.

[JT93] D. S. Johnson and M. A. Trick. The second dimacs implementa

tion challenge. In DIMACS Series in Discrete Mathematics and
Theoritical Computer Science, 1993.

[McM00] K. L. McMillan. The smv system for smv version 2.5.4. In
Carnegie

Mellon University, 2000.

[SC85] A. P. Sistla and E. M. Clarke. The complexity of
propositional linear temporal logics. In Journal of Assoc. Comput. 
Mach., pages 733-749, 1985.

[SS98] Mary Sheeran and Gunnar Stalmarck. A tutorial on
stalmarcks's

proof procedure for propositional logic. In Formal Methods in
Computer-Aided Design, pages 82-99, 1998.