World Library  
Flag as Inappropriate
Email this Article

Edmund M. Clarke

Article Id: WHEBN0015590926
Reproduction Date:

Title: Edmund M. Clarke  
Author: World Heritage Encyclopedia
Language: English
Subject: Robert Lee Constable, List of pioneers in computer science, List of Turing Award laureates by university affiliation, Robert Tarjan, Adi Shamir
Collection: 1945 Births, American Computer Scientists, Carnegie Mellon University Faculty, Cornell University Alumni, Duke University Alumni, Duke University Faculty, Fellow Members of the Ieee, Fellows of the American Academy of Arts and Sciences, Fellows of the Association for Computing MacHinery, Formal Methods People, Harvard University Faculty, Living People, Members of the United States National Academy of Engineering, Turing Award Laureates, University of Virginia Alumni
Publisher: World Heritage Encyclopedia

Edmund M. Clarke

Edmund M. Clarke

Edmund Melson Clarke, Jr. (born July 27, 1945) is a computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He is the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, is a recipient of the 2007 Association for Computing Machinery A.M. Turing Award.


  • Biography 1
  • Work 2
  • Professional recognition 3
  • External links 4


Clarke received a B.A. degree in mathematics from the University of Virginia, Charlottesville, VA, in 1967, an M.A. degree in mathematics from Duke University, Durham NC, in 1968, and a Ph.D. degree in Computer Science from Cornell University, Ithaca NY in 1976. After receiving his Ph.D., he taught in the Department of Computer Science at Duke University, for two years. In 1978 he moved to Harvard University, Cambridge, MA where he was an Assistant Professor of Computer Science in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA. He was appointed Full Professor in 1989. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the Carnegie Mellon School of Computer Science.


Clarke's interests include software and hardware verification and automatic theorem proving. In his Ph.D. thesis he proved that certain programming language control structures did not have good Hoare style proof systems. In 1981 he and his Ph.D. student E. Allen Emerson first proposed the use of model checking as a verification technique for finite state concurrent systems. His research group pioneered the use of model checking for hardware verification. Symbolic model checking using BDDs was also developed by his group. This important technique was the subject of Kenneth McMillan's Ph.D. thesis, which received an ACM Doctoral Dissertation Award. In addition, his research group developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica). In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems (CMACS) center, funded by the National Science Foundation. This center has a team of researchers, spanning multiple universities, applying abstract interpretation and model checking to biological and embedded systems.

Professional recognition

Clarke is a fellow of the ACM and the IEEE. He received a Technical Excellence Award from the Semiconductor Research Corporation in 1995 and an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department in 1999. He was a co-winner along with Randal Bryant, E. Allen Emerson, and Kenneth McMillan of the ACM Paris Kanellakis Award in 1999 for the development of symbolic model checking. In 2004 he received the IEEE Computer Society Harry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was elected to the American Academy of Arts and Sciences in 2011. He received the Herbrand Award in 2008 in “recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades.” He received the 2014 Bower Award and Prize for Achievement in Science from the Franklin Institute for “his leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems, including those found in transportation, communications, and medicine.” He is a member of Sigma Xi and Phi Beta Kappa.

External links

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from World Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.