Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia in 1967, a M.A. degree in mathematics from Duke University in 1968, and a Ph.D. degree in computer science from Cornell in 1976. He taught at Duke University from 1976-1978 and at Harvard University from 1978-1982. Since 1982 he has been on the faculty in the Computer Science Department at Carnegie-Mellon University. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008 and became Professor Emeritus in Aug 2015.
Dr. Clarke's interests include software and hardware verification and automatic theorem proving. In 1981 he and a graduate student, 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 and software verification. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of CounterExample-Guided-Abstraction-Refinement (CEGAR). In addition, Clarke and his students developed the first parallel general resolution theorem prover (Parthenon), and the first theorem prover to be based on a symbolic computation system (Analytica).
Dr. Clarke is co-founder of the conference on Computer Aided Verification (CAV) and served on its steering committee for many years. He is the former editor-in-chief of Formal Methods in Systems Design. He served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. In 1995 he received a Technical Excellence Award from the Semiconductor Research Corporation. He was a co-recipient of the ACM Kanellakis Award in 1998 for the invention of symbolic model checking. In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department.
In 2004 Dr. Clarke received the IEEE Harry H. Goode Memorial Award for significant and pioneering contribution to formal verification of hardware and software systems. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was a co-recipient of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award for the paper "Symbolic Modelc Checking: 1020 States and Beyond"and from ETAPS in 2017 for “Symbolic model-checking without BDDs”.
Dr. Clarke was elected to the American Academy of Arts and Sciences in 2011. He received an Honorary Doctorate from the Vienna University of Technology in 2012 and from the University of Crete in 2014 , and the Technion-Israel Institute of Technology in 2016. The Chinese Academy of Sciences awarded him an Einstein Professorship in 2013. He received the Franklin Institute 2014 Bower Award and Prize for Achievement in Science for his leading role in the conception and development of techniques for verification of computer systems. Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.
Edmund M. Clarke is now Professor Emeritus in the Computer Science Department at Carnegie Mellon University. He was the first recipient of the FORE Systems Endowed Professorship in 1995 and became a University Professor in 2008. He received a B.A. degree from the University of Virginia, a M.S. degree from Duke University, a Ph.D. from Cornell University, and taught at Duke and Harvard Universities before joining CMU in 1982. His research interests include hardware and software verification and automatic theorem proving. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of CounterExample-Guided-Abstraction-Refinement (CEGAR). He was a co-founder of the conference on Computer Aided Verification (CAV). He has received numerous awards for his contributions to formal verification of hardware and software correctness, including the IEEE Goode Award, ACM Kanellakis Award, ACM Turing Award, CADE Herbrand Award, and the CAV Award. He received the 2014 Franklin Institute Bower Award and Prize for Achievement in Science for verification of computer systems. He received an Einstein Professorship from the Chinese Academy of Sciences and honorary doctorates from the Vienna University of Technology, the University of Crete, and the Technion-Israel Institute of Technology. Dr. Clarke is a member of the National Academy of Engineering and the American Academy of Arts and Sciences, a Fellow of the ACM and IEEE, and member of Sigma Xi and Phi Beta Kappa.