Model Checking
Edmund M. Clarke, Orna Grumberg and Doron A. Peled
MIT Press, 1999.

• Birth of Model Checking. 25 Years of Model checking, vol. 5000, 2008. PDF
  
  
• E. Clarke, O. Grumberg and D. Long. Verification tools for finite-state concurrent systems. In: A Decade of concurrency--Reflections and Perspectives . Lecture Notes in Computer Science, 803, 1994.

• J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 10E20 states and beyond. In LICS, 1990.

• E.M. Clarke, O. Grumberg,H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. Verfication of the Futurebus+cache coherence protocol. In L. Claesen, editor, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.
 
• W. Marrero, E.M. Clarke, and S. Jha. Model Checking for Security Protocols. Technical Report CMU-SCS-97-139, Carnegie Mellon University, May 1997.
 
• E.M.Clarke and E.A. Emerson and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In ACM Transactions on Programming Languages and Systems, 8(2):244- 263, 1986.
 
• E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981 Lecture Notes in Computer Science, vol. 131, Springer-Verlag. 1981.
  

For a complete list of all my papers, consult my Curriculum Vitae.

Electronic versions of many of my papers can obtained from the Publications web page.

For a description of current research, see CMU Model Checking home page.