Edmund Melson Clarke
Born 27 July 1945, Newport News, Virginia, USA
Turing Award (2007), “together with E. Allen Emerson and Joseph Sifakis, for their role in developing Model Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.”
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 University 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.
In addition to the Turing Award, Dr. Clarke was a co-recipient of the ACM Kanellakis Award in 1998. In 2004 Dr. Clarke received the IEEE Harry H. Goode Memorial Award. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award. In 2011 he was elected to the American Academy of Arts and Sciences. He received an Honorary Doctorate from the Vienna University of Technology in 2012. In 2013 he was awarded an Einstein Professorship by the Chinese Academy of Sciences.
Dr. Clarke’s research 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 at Carnegie Mellon pioneered the use of Model Checking for hardware and software verification. In particular, his group developed Symbolic Model Checking using Binary Decision Diagrams (BDDs), Bounded Model Checking using fast 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).
In Model Checking specifications are written that describe an abstract model in a logic that allows temporal statements, such as “if break is applied, then vehicle will de-accelerate”. The abstract model is simply a formalization of the hardware and software to be tested. The initial states of the model must satisfy the formula. If not, the model checker will find a counterexample execution trace in the model that illustrates why the specification is not satisfied. The method allows Model Checking to be done automatically via computer. Model Checking can determine, for example, the correctness of digital circuits or the synchronization skeleton of a complex program. If the design contains an error, then the algorithm flags the situation in which the error occurs, alerting the user to the possible need for a correction.