Edmund Melson ClarkeProfessor Emeritus

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.