Edmund M. Clarke
Encyclopedia
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 winner of the 2007 Association for Computing Machinery
A.M. Turing Award
.
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
.
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).
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 is a member of Sigma Xi
and Phi Beta Kappa.
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
and academic noted for developing
model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, a method for formally verifying hardware and software designs.
He is the FORE Systems
FORE Systems
FORE Systems was a computer network switching equipment company based in Pittsburgh, Pennsylvania. The company is now part of Ericsson.-History:...
Professor of Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
at Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
. Clarke, along with E. Allen Emerson
E. Allen Emerson
Ernest Allen Emerson is a computer scientist and endowed professor at the University of Texas, Austin, USA.He won the 2007 A.M. Turing Award along with Edmund M...
and Joseph Sifakis
Joseph Sifakis
Joseph Sifakis is a Greek-French computer scientist, laureate of the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking....
, is a winner of the 2007 Association for Computing Machinery
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
A.M. Turing Award
Turing Award
The Turing Award, in full The ACM A.M. Turing Award, is an annual award given by the Association for Computing Machinery to "an individual selected for contributions of a technical nature made to the computing community. The contributions should be of lasting and major technical importance to the...
.
Biography
Clarke received a B.A.Bachelor of Arts
A Bachelor of Arts , from the Latin artium baccalaureus, is a bachelor's degree awarded for an undergraduate course or program in either the liberal arts, the sciences, or both...
degree in mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
from the University of Virginia
University of Virginia
The University of Virginia is a public research university located in Charlottesville, Virginia, United States, founded by Thomas Jefferson...
, Charlottesville, VA
Charlottesville, Virginia
Charlottesville is an independent city geographically surrounded by but separate from Albemarle County in the Commonwealth of Virginia, United States, and named after Charlotte of Mecklenburg-Strelitz, the queen consort of King George III of the United Kingdom.The official population estimate for...
, in 1967, an M.A.
Master of Arts (postgraduate)
A Master of Arts from the Latin Magister Artium, is a type of Master's degree awarded by universities in many countries. The M.A. is usually contrasted with the M.S. or M.Sc. degrees...
degree in mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
from Duke University
Duke University
Duke University is a private research university located in Durham, North Carolina, United States. Founded by Methodists and Quakers in the present day town of Trinity in 1838, the school moved to Durham in 1892. In 1924, tobacco industrialist James B...
, Durham NC
Durham, North Carolina
Durham is a city in the U.S. state of North Carolina. It is the county seat of Durham County and also extends into Wake County. It is the fifth-largest city in the state, and the 85th-largest in the United States by population, with 228,330 residents as of the 2010 United States census...
, in 1968, and a Ph.D.
Doctor of Philosophy
Doctor of Philosophy, abbreviated as Ph.D., PhD, D.Phil., or DPhil , in English-speaking countries, is a postgraduate academic degree awarded by universities...
degree in Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
from Cornell University
Cornell University
Cornell University is an Ivy League university located in Ithaca, New York, United States. It is a private land-grant university, receiving annual funding from the State of New York for certain educational missions...
, Ithaca NY
Ithaca, New York
The city of Ithaca, is a city in upstate New York and the county seat of Tompkins County, as well as the largest community in the Ithaca-Tompkins County metropolitan area...
in 1976. After receiving his Ph.D., he taught in the Department of Computer Science at Duke University
Duke University
Duke University is a private research university located in Durham, North Carolina, United States. Founded by Methodists and Quakers in the present day town of Trinity in 1838, the school moved to Durham in 1892. In 1924, tobacco industrialist James B...
, for two years. In 1978 he moved to Harvard University
Harvard University
Harvard University is a private Ivy League university located in Cambridge, Massachusetts, United States, established in 1636 by the Massachusetts legislature. Harvard is the oldest institution of higher learning in the United States and the first corporation chartered in the country...
, Cambridge, MA
Cambridge, Massachusetts
Cambridge is a city in Middlesex County, Massachusetts, United States, in the Greater Boston area. It was named in honor of the University of Cambridge in England, an important center of the Puritan theology embraced by the town's founders. Cambridge is home to two of the world's most prominent...
where he was an Assistant Professor of Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
, Pittsburgh, PA
Pittsburgh, Pennsylvania
Pittsburgh is the second-largest city in the US Commonwealth of Pennsylvania and the county seat of Allegheny County. Regionally, it anchors the largest urban area of Appalachia and the Ohio River Valley, and nationally, it is the 22nd-largest urban area in the United States...
. He was appointed Full Professor in 1989. In 1995 he became the first recipient of the FORE Systems
FORE Systems
FORE Systems was a computer network switching equipment company based in Pittsburgh, Pennsylvania. The company is now part of Ericsson.-History:...
Professorship, an endowed chair in the Carnegie Mellon School of Computer Science
Carnegie Mellon School of Computer Science
The School of Computer Science at Carnegie Mellon University in Pittsburgh, Pennsylvania, USA is a leading private school for computer science established in 1965. It has been consistently ranked among the top computer science programs over the decades. U.S...
.
Work
Clarke's interests include software and hardwareHardware
Hardware is a general term for equipment such as keys, locks, hinges, latches, handles, wire, chains, plumbing supplies, tools, utensils, cutlery and machine parts. Household hardware is typically sold in hardware stores....
verification
Verification and Validation
In software project management, software testing, and software engineering, verification and validation is the process of checking that a software system meets specifications and that it fulfills its intended purpose...
and automatic theorem proving. In his Ph.D. thesis he proved that certain programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
control structures did not have good Hoare style proof systems
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
. In 1981 he and his Ph.D. student E. Allen Emerson
E. Allen Emerson
Ernest Allen Emerson is a computer scientist and endowed professor at the University of Texas, Austin, USA.He won the 2007 A.M. Turing Award along with Edmund M...
first proposed the use of Model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
as a verification technique for finite state concurrent systems
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
. His research group pioneered the use of Model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
for hardware verification. Symbolic Model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
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
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
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).
Professional recognition
Clarke is a fellowFellow
A fellow in the broadest sense is someone who is an equal or a comrade. The term fellow is also used to describe a person, particularly by those in the upper social classes. It is most often used in an academic context: a fellow is often part of an elite group of learned people who are awarded...
of the ACM
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
and the IEEE. He received a Technical Excellence Award from the Semiconductor Research Corporation
Semiconductor Research Corporation
Celebrating 29 years of collaborative research for the semiconductor industry, Semiconductor Research Corporation is the world's leading technology research consortium...
in 1995 and an Allen Newell
Allen Newell
Allen Newell was a researcher in computer science and cognitive psychology at the RAND corporation and at Carnegie Mellon University’s School of Computer Science, Tepper School of Business, and Department of Psychology...
Award for Excellence in Research from the Carnegie Mellon Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
Department in 1999. He was a co-winner along with Randal Bryant
Randal Bryant
Randal E. Bryant is an American computer scientist and academic noted for his research on formally verifying digital hardware, and more recently some forms of software...
, E. Allen Emerson
E. Allen Emerson
Ernest Allen Emerson is a computer scientist and endowed professor at the University of Texas, Austin, USA.He won the 2007 A.M. Turing Award along with Edmund M...
, and Kenneth McMillan of the ACM
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
Paris Kanellakis Award
Paris Kanellakis Award
The Paris Kanellakis Theory and Practice Award is granted yearly by the Association for Computing Machinery to honor specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing...
in 1999 for the development of Symbolic Model Checking. In 2004 he received the IEEE Computer Society
IEEE Computer Society
The IEEE Computer Society is a professional society of IEEE. Its purpose and scope is “to advance the theory, practice, and application of computer and information processing science and technology” and the “professional standing of its members.” The CS is the largest of 38 technical societies...
Harry H. Goode
Harry H. Goode
Harry H. Goode was an American computer engineer and systems engineer and professor at the University of Michigan. He is known as co-author of the book Systems Engineering from 1957, which is one of the earliest significant books directly related to systems engineering.-Biography:Harry Goode was...
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
National Academy of Engineering
The National Academy of Engineering is a government-created non-profit institution in the United States, that was founded in 1964 under the same congressional act that led to the founding of the National Academy of Sciences...
in 2005 for contributions to the formal verification of hardware and software correctness. He is a member of Sigma Xi
Sigma Xi
Sigma Xi: The Scientific Research Society is a non-profit honor society which was founded in 1886 at Cornell University by a junior faculty member and a handful of graduate students. Members elect others on the basis of their research achievements or potential...
and Phi Beta Kappa.