Edmund Clarke's Biography
Edmund M. 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, 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 School
of Computer Science.
Dr. 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 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 resarch group developed the first parallel resolution
theorem prover (Parthenon) and the first theorem prover to
be based on a symbolic computation system (Analytica).
Dr. Clarke has served on the editorial boards of Distributed
Computing, Logic and Computation, and IEEE Transactions in
Software Engineering. He is the former editor-in-chief of
Formal Methods in Systems Design. He is on the organizing
committee of Logic in Computer Science (LICS) and on the steering
committee of Computer-Aided Verification (CAV). 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 Randy Bryant, Allen Emerson, and Kenneth McMillan
of the ACM Kanellakis Award in 1999
for the development of Symbolic Model Checking.
In 2004 he received the IEEE 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.
Dr. Clarke is a Fellow of the Association
for Computing Machinery and the IEEE Computer Society,
and a member of Sigma Xi and Phi Beta Kappa.
|
