Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American

computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...

and

academic An academy (Attic Greek: Ἀκαδήμεια; Koine Greek Ἀκαδημία) is an institution of secondary education, secondary or tertiary education, tertiary higher education, higher learning (and generally also research or honorary membershi ...

noted for developing

model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...

, a method for formally verifying hardware and software designs. He was the

FORE Systems FORE Systems was a computer network switching equipment company based in Pittsburgh, Pennsylvania. Founded in 1990 to supply Asynchronous Transfer Mode (ATM) cards for workstation computers, it soon branched out to become a major supplier in the AT ...

Professor of

Computer Science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...

. Clarke, along with

E. Allen Emerson Ernest Allen Emerson II (born June 2, 1954), better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States. ...

and

Joseph Sifakis Joseph Sifakis (Greek: Ιωσήφ Σηφάκης) is a Greek- French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking. Biography Joseph Sifakis was born in He ...

, received the 2007

ACM ACM or A.C.M. may refer to: Aviation * AGM-129 ACM, 1990–2012 USAF cruise missile * Air chief marshal * Air combat manoeuvring or dogfighting * Air cycle machine * Arica Airport (Colombia) (IATA: ACM), in Arica, Amazonas, Colombia Computing * ...

Turing Award The ACM A. M. Turing Award is an annual prize given by the Association for Computing Machinery (ACM) for contributions of lasting and major technical importance to computer science. It is generally recognized as the highest distinction in compu ...

Biography

Born in

Newport News, Virginia Newport News () is an independent city in the U.S. state of Virginia. At the 2020 census, the population was 186,247. Located in the Hampton Roads region, it is the 5th most populous city in Virginia and 140th most populous city in the Uni ...

, Clarke received a

B.A. Bachelor of arts (BA or AB; from the Latin ', ', or ') is a bachelor's degree awarded for an undergraduate program in the arts, or, in some cases, other disciplines. A Bachelor of Arts degree course is generally completed in three or four years ...

degree in

mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

from the

University of Virginia The University of Virginia (UVA) is a Public university#United States, public research university in Charlottesville, Virginia. Founded in 1819 by Thomas Jefferson, the university is ranked among the top academic institutions in the United S ...

Charlottesville Charlottesville, colloquially known as C'ville, is an independent city in the Commonwealth of Virginia. It is the county seat of Albemarle County, which surrounds the city, though the two are separate legal entities. It is named after Queen Cha ...

, in 1967, an

M.A. A Master of Arts ( la, Magister Artium or ''Artium Magister''; abbreviated MA, M.A., AM, or A.M.) is the holder of a master's degree awarded by universities in many countries. The degree is usually contrasted with that of Master of Science. Tho ...

degree in

from

Duke University Duke University is a private research university in Durham, North Carolina. Founded by Methodists and Quakers in the present-day city of Trinity in 1838, the school moved to Durham in 1892. In 1924, tobacco and electric power industrialist James ...

, Durham NC, in 1968, and a

Ph.D. A Doctor of Philosophy (PhD, Ph.D., or DPhil; Latin: or ') is the most common degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields. Because it is a ...

degree in

from

Cornell University Cornell University is a private statutory land-grant research university based in Ithaca, New York. It is a member of the Ivy League. Founded in 1865 by Ezra Cornell and Andrew Dickson White, Cornell was founded with the intention to teach an ...

, Ithaca NY in 1976. After receiving his Ph.D., he taught in the Department of Computer Science at

, for two years. In 1978, he moved to

Harvard University Harvard University is a private Ivy League research university in Cambridge, Massachusetts. Founded in 1636 as Harvard College and named for its first benefactor, the Puritan clergyman John Harvard, it is the oldest institution of higher le ...

Cambridge, MA Cambridge ( ) is a city in Middlesex County, Massachusetts, United States. As part of the Boston metropolitan area, the cities population of the 2020 U.S. census was 118,403, making it the fourth most populous city in the state, behind Boston ...

where he was an assistant professor of

in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at

Pittsburgh, PA Pittsburgh ( ) is a city in the Commonwealth of Pennsylvania, United States, and the county seat of Allegheny County. It is the most populous city in both Allegheny County and Western Pennsylvania, the second-most populous city in Pennsyl ...

. He was appointed Full Professor in 1989. In 1995, he became the first recipient of the

Professorship, an endowed chair in the

Carnegie Mellon School of Computer Science The School of Computer Science (SCS) at Carnegie Mellon University in Pittsburgh, Pennsylvania, US is a school for computer science established in 1988. It has been consistently ranked among the top computer science programs over the decades. A ...

. He became a University Professor in 2008 and became an emeritus professor in 2015. He died from

COVID-19 Coronavirus disease 2019 (COVID-19) is a contagious disease caused by a virus, the severe acute respiratory syndrome coronavirus 2 (SARS-CoV-2). The first known case was COVID-19 pandemic in Hubei, identified in Wuhan, China, in December ...

in December 2020, at age 75, during the

COVID-19 pandemic in Pennsylvania The COVID-19 pandemic was confirmed to have reached the U.S. state of Pennsylvania in March 2020. , the Pennsylvania Department of Health has confirmed 1,464,264 cumulative cases and 29,814 deaths in the state. , Pennsylvania has administered 6 ...

Work

Clarke's interests included

software Software is a set of computer programs and associated documentation and data. This is in contrast to hardware, from which the system is built and which actually performs the work. At the lowest programming level, executable code consists ...

and hardware

verification Verify or verification may refer to: General * Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...

and automatic theorem proving. In his Ph.D. thesis he proved that certain

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

control structures did not have good Hoare-style proof systems. In 1981 he and his Ph.D. student

first proposed the use of

as a verification technique for finite state concurrent systems. His research group pioneered the use of

for

hardware verification Electronic design automation (EDA), also referred to as electronic computer-aided design (ECAD), is a category of software tools for designing electronic systems such as integrated circuits and printed circuit boards. The tools work together ...

. Symbolic

using

binary decision diagrams In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Un ...

was also developed by his group. This important technique was the subject of Kenneth McMillan's Ph.D. thesis, which received an

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). In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems (CMACS) center, funded by the

National Science Foundation The National Science Foundation (NSF) is an independent agency of the United States government that supports fundamental research and education in all the non-medical fields of science and engineering. Its medical counterpart is the National I ...

. This center has a team of researchers, spanning multiple universities, applying

abstract interpretation In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer prog ...

and

to biological and embedded systems.

Professional recognition

Clarke was a

fellow A fellow is a concept whose exact meaning depends on context. In learned or professional societies, it refers to a privileged member who is specially elected in recognition of their work and achievements. Within the context of higher education ...

of the

and the

IEEE The Institute of Electrical and Electronics Engineers (IEEE) is a 501(c)(3) professional association for electronic engineering and electrical engineering (and associated disciplines) with its corporate office in New York City and its operation ...

. He received a Technical Excellence Award from the

Semiconductor Research Corporation Semiconductor Research Corporation (SRC), commonly known as SRC, is a high-technology research consortium active in the semiconductor industry. It is a leading semiconductor research consortium. Todd Younkin is the incumbent president and chief e ...

in 1995 and an

Allen Newell Allen Newell (March 19, 1927 – July 19, 1992) 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 ...

Award for Excellence in Research from the

Carnegie Mellon Carnegie may refer to: People * Carnegie (surname), including a list of people with the name * Clan Carnegie, a lowland Scottish clan Institutions Named for Andrew Carnegie *Carnegie Building (Troy, New York), on the campus of Rensselaer Polyt ...

Department in 1999. He was a co-winner along with

Randal Bryant Randal E. Bryant (born October 27, 1952) is an American computer scientist and academic noted for his research on formally verifying digital hardware and software. Bryant has been a faculty member at Carnegie Mellon University since 1984. He ser ...

, and Kenneth McMillan of the

Paris Kanellakis Award The Paris Kanellakis Theory and Practice Award is granted yearly by the Association for Computing Machinery (ACM) to honor "specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing". It wa ...

in 1999 for the development of symbolic model checking. In 2004 he received the

IEEE Computer Society The Institute of Electrical and Electronics Engineers (IEEE) is a 501(c)(3) professional association for electronic engineering and electrical engineering (and associated disciplines) with its corporate office in New York City and its operati ...

Harry H. Goode Harry H. Goode (June 30, 1909 – October 30, 1960) 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 earl ...

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 The National Academy of Engineering (NAE) is an American nonprofit, non-governmental organization. The National Academy of Engineering is part of the National Academies of Sciences, Engineering, and Medicine, along with the National Academy ...

in 2005 for contributions to the formal verification of hardware and software correctness. He was elected to the

American Academy of Arts and Sciences The American Academy of Arts and Sciences (abbreviation: AAA&S) is one of the oldest learned societies in the United States. It was founded in 1780 during the American Revolution by John Adams, John Hancock, James Bowdoin, Andrew Oliver, and ...

in 2011. He received the

Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important cont ...

in 2008 in "recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades." In 2012, h
received an honorary doctorate
from

TU Wien TU Wien (TUW; german: Technische Universität Wien; still known in English as the Vienna University of Technology from 1975–2014) is one of the major universities in Vienna, Austria. The university finds high international and domestic recogn ...

for his outstanding contributions to the field of informatics. He received the 2014

Bower Award and Prize for Achievement in Science Bower may refer to: Arts and entertainment * ''Catherine, or The Bower'', an unfinished Jane Austen novel * A high-ranking card (usually a Jack) in certain card games: ** The Right and Left Bower (or Bauer), the two highest-ranking cards in the g ...

from the

Franklin Institute The Franklin Institute is a science museum and the center of science education and research in Philadelphia, Pennsylvania. It is named after the American scientist and statesman Benjamin Franklin. It houses the Benjamin Franklin National Memori ...

for "his leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems, including those found in transportation, communications, and medicine." He was a member of

Sigma Xi Sigma Xi, The Scientific Research Honor Society () is a highly prestigious, non-profit honor society for scientists and engineers. Sigma Xi was founded at Cornell University by a junior faculty member and a small group of graduate students in 1886 ...

and

Phi Beta Kappa The Phi Beta Kappa Society () is the oldest academic honor society in the United States, and the most prestigious, due in part to its long history and academic selectivity. Phi Beta Kappa aims to promote and advocate excellence in the liberal a ...

References

External links

*
Home page at Carnegie Mellon University

Turing Award announcement

Model Checking book

CMACS home page
* {{DEFAULTSORT:Clarke, Edmund 1945 births 2020 deaths People from Newport News, Virginia American computer scientists Carnegie Mellon University faculty University of Virginia alumni Duke University alumni Cornell University alumni Duke University faculty John A. Paulson School of Engineering and Applied Sciences faculty Fellows of the Association for Computing Machinery Fellow Members of the IEEE Turing Award laureates Fellows of the American Academy of Arts and Sciences Members of the United States National Academy of Engineering Formal methods people Scientists from Virginia Deaths from the COVID-19 pandemic in Pennsylvania

Biography

Work

Professional recognition

See also

References

External links