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 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. 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 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.