• Model Checking: Second Edition
  Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, & Helmut Veith, MIT Press, 2018

• LNCS Contributions by Edmund M. Clarke
  
  
• Birth of Model Checking. 25 Years of Model checking: Lecture notes in Computer Science, vol. 5000, 2008. PDF


• Counterexample-guided abstraction refinement for symbolic model checking. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, J.ACM 50 (5): 752-794 (2003). PDF


• Bounded model checking using satisfiability solving. E. M. Clarke, A. Biere, R. Raimi, Y. Zhu, Formal Methods in System Design 19 (1): 7-34 (2001). PDF

• Verification tools for finite-state concurrent systems. E. Clarke, O. Grumberg and D. Long. In: A Decade of concurrency--Reflections and Perspectives . Lecture Notes in Computer Science, 803, 1994. PDF
  
  
• Verfication of the Futurebus+cache coherence protocol. E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. In L. Claesen, editor, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993. PDF
  
  
• Symbolic model checking: 10²⁰ states and beyond. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. In LICS, 1990. PDF
  
  
• Automatic verification of finite-state concurrent systems using temporal logic specifications. E.M.Clarke, E.A. Emerson, and A.P. Sistla. In ACM Transactions on Programming Languages and Systems, 8(2):244- 263, 1986. PDF


• Design and synthesis of synchronization skeletons using branching time  temporal logic. E.M. Clarke and E.A. Emerson. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981 Lecture Notes in Computer Science, vol. 131, Springer-Verlag. 1981. PDF
  
  
  

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.