National Academies Press: OpenBook

Memorial Tributes: Volume 24 (2022)

Chapter: EDMUND M. CLARKE

« Previous: BRUNO A. BOLEY
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

Image

Image

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

EDMUND M. CLARKE

1945–2020

Elected in 2005

“For contributions to the formal verification of hardware and software correctness.”

BY RANDAL E. BRYANT

EDMUND MELSON CLARKE JR., formerly the FORE Systems University Professor of Computer Science at Carnegie Mellon University and cowinner of the 2007 ACM Turing Award, died December 22, 2020, of covid-19, after a long illness. He was 75.

Ed was born July 27, 1945, and grew up in Smithfield, Virginia, before attending the University of Virginia and studying mathematics; he got his bachelor’s degree in 1967. Following receipt the next year of a master’s degree in mathematics from Duke University, he switched to computer science and earned a PhD from Cornell University in 1976. From there he went on to faculty positions at Duke and Harvard until he was hired in 1982 in the Computer Science Department at Carnegie Mellon University (CMU), where he remained until his retirement in 2015.

Early in his career, Ed took on the challenge of finding ways to ensure that hardware and software systems operate as they should, especially systems that must handle multiple activities with uncertain timing. While at Harvard, he and his graduate student Allen Emerson devised an approach they called “model checking” and published their first paper on the topic in 1981. Their idea was to describe the possible actions of a system in temporal logic, a formal notation for describing

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

events occurring in time without explicitly using time values. For example, temporal logic can encode the statement “If a car approaches a traffic light, the light will eventually turn green.” A model checker then exhaustively considers all possible ways the system can operate and either determines that all of them satisfy the specification, or it provides a specific case where the system may misbehave. This “counterexample” can then be used by the designer in debugging the system design.

Model checking was a novel idea when introduced. At the time, to formally verify computer systems, methods researchers were simply using extensions of methods that humans used to prove mathematical statements, in terms of lemmas, theorems, and their proofs. Model checking did not require any human reasoning or intervention. It took advantage of the power of computers to systematically consider the many cases that could arise during system operation.

The original model checkers were limited to very simple systems and protocols, since the number of possible states of a system can grow exponentially with the number of memory elements—a single 64-bit computer word can have over 1019 different values. This limitation was overcome in 1987 when Ed’s graduate student Ken McMillan recognized that the analysis required for model checking could be performed symbolically, without explicitly enumerating state values. Just as Pythagoras didn’t have to prove that a2 + b2 = c2 by drawing and measuring a bunch of right triangles, a symbolic model checker can encode the possible states of a system in symbolic form and manipulate these representations algorithmically. In this case, Ken made use of the ordered binary decision diagram (BDD) representation and algorithms that I had published the year before.

Symbolic model checking became a breakthrough technology for the computer industry. Major companies, such as IBM, Intel, and Fujitsu, developed their own model checkers and applied them to their system designs. They were especially effective at verifying the then new protocols used by multiprocessor systems to maintain a consistent memory state, despite having values stored across multiple cache memories.

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

In 2002 a group at Microsoft Research devised a model checker for abstracted forms of software, enabling them to automatically verify the operating system code used to operate external devices. This tool was made available to the large number of third-party software developers writing device drivers for the Windows operating system. Use of this tool vastly decreased occurrences of the “blue screen of death” when the computer reached a deadlock condition.

Ed, his graduate students, and his postdoctoral researchers remained at the forefront of model checking research. Starting in 2009, Ed led the NSF-sponsored Computational Models and Analysis for Complex Systems Center, which applied model checking and related methods for software verification to problems in the areas of pancreatic cancer modeling, atrial-fibrillation detection, distributed automotive control, and aerospace control software. His PhD students and former postdocs have gone on to successful academic and industry careers throughout the world.

Over his career, Ed was recognized with many awards and honors, both for his intellectual contribution of model checking (and the vast research community it engendered) and for the practical impacts of his ideas on real-world hardware and software. He received the 2004 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.” The next year he was elected to the NAE. In 2007 the ACM Turing Award—sometimes referred to as the “Nobel Prize of Computer Science”—was presented jointly to him, Allen Emerson, and Joseph Sifakis of France, who had independently devised an approach very similar to model checking around the same time as Clarke and Emerson. They were cited “for their role in developing model checking into a highly effective verification technology that is widely adopted in the hardware and software industries.” Ed also received the International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning (2008), and in 2014 the

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

Bower Award and Prize for Achievement in Science from the Franklin Institute. He was elected to the American Academy of Arts and Sciences and was a fellow of the ACM and IEEE.

Ed is survived by his wife, Martha, whom he met in high school. They were married for over 50 years. Their three sons have had successful careers themselves: James, director of Quantum Hardware at Intel Corporation in Portland, Oregon; Jonathan, a professor in the business school at Georgia Tech; and Jeffrey, an oncologist at Duke University Hospital. There are currently six grandchildren. Ed was an active member of the Mt. Lebanon United Methodist Church.

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×

This page intentionally left blank.

Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 44
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 45
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 46
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 47
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 48
Suggested Citation:"EDMUND M. CLARKE." National Academy of Engineering. 2022. Memorial Tributes: Volume 24. Washington, DC: The National Academies Press. doi: 10.17226/26492.
×
Page 49
Next: ARCHIE R. CLEMINS »
Memorial Tributes: Volume 24 Get This Book
×
Buy Hardback | $107.00
MyNAP members save 10% online.
Login or Register to save!
Download Free PDF

This is the twenty-fourth volume in the Memorial Tributes series compiled by the National Academy of Engineering as a personal remembrance of the lives and outstanding achievements of its members and international members. These volumes are intended to stand as an enduring record of the many contributions of engineers and engineering to the benefit of humankind. In most cases, the authors of the tributes are contemporaries or colleagues who have personal knowledge of the interests and engineering accomplishments of the deceased.

  1. ×

    Welcome to OpenBook!

    You're looking at OpenBook, NAP.edu's online reading room since 1999. Based on feedback from you, our users, we've made some improvements that make it easier than ever to read thousands of publications on our website.

    Do you want to take a quick tour of the OpenBook's features?

    No Thanks Take a Tour »
  2. ×

    Show this book's table of contents, where you can jump to any chapter by name.

    « Back Next »
  3. ×

    ...or use these buttons to go back to the previous chapter or skip to the next one.

    « Back Next »
  4. ×

    Jump up to the previous page or down to the next one. Also, you can type in a page number and press Enter to go directly to that page in the book.

    « Back Next »
  5. ×

    Switch between the Original Pages, where you can read the report as it appeared in print, and Text Pages for the web version, where you can highlight and search the text.

    « Back Next »
  6. ×

    To search the entire text of this book, type in your search term here and press Enter.

    « Back Next »
  7. ×

    Share a link to this book page on your preferred social network or via email.

    « Back Next »
  8. ×

    View our suggested citation for this chapter.

    « Back Next »
  9. ×

    Ready to take your reading offline? Click here to buy this book in print or download it as a free PDF, if available.

    « Back Next »
Stay Connected!