Edmund M. Clarke, a professor emeritus at Carnegie Mellon University who won computer science's equivalent of the Nobel Prize, died Tuesday of COVID-19 after a long illness. He was 75.
Mr. Clarke, of Mt. Lebanon, was best known for his work in model checking, an automated method for detecting design errors in computer hardware and software.
CMU president Farnam Jahanian said the world had “lost a giant in computer science” with Mr. Clarke’s death.
“Ed’s pioneering work in model checking applied formal computational methods to the ultimate challenge: computers checking their own correctness,” Mr. Jahanian said in a statement. “As systems become ever more complex, we are just beginning to see the wide-reaching and long-term benefits of Ed's insights, which will continue to inspire researchers and practitioners for years to come.”
In the early 1980s, Mr. Clarke and his Harvard University graduate student, E. Allen Emerson — as well as Joseph Sifakis of the University of Grenoble, who was working separately — developed model checking, which has helped to improve the reliability of complex computer chips, systems and networks.
For their work, the Association for Computing Machinery gave the three scientists the prestigious A.M. Turing Award — computer science’s Nobel Prize — in 2007.
Mr. Clark’s citation on the Turing Award website said Microsoft and Intel and other companies use model checking to verify designs for computer networks and software.
“It is becoming particularly important in the verification of software designed for recent generations of integrated circuits, which feature multiple processors running simultaneously,” the citation page said. “Model checking has substantially improved the reliability and safety of the systems upon which modern life depends.”
Model checking allowed engineers to analyze the logic beneath a design similar to how a mathematician uses a proof to determine that a theorem is correct, according to CMU. It considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications.
Before the development of model checking, CMU said, engineers checked for logic errors in computer circuitry or software programs by running simulations to test performance as well as manually examining each line of computer code. But those methods became inadequate as computers became more complex, and errors often went undetected until after a product was released, which could be costly even when minor, according to the university.
Mr. Clarke joined the computer science faculty at CMU in 1982. In 1995, was the first recipient of an endowed chair in the School of Computer Science called the FORE Systems Professorship.
Before arriving at CMU, Mr. Clarke taught at Duke University and Harvard University. He received a bachelor’s degree in mathematics from the University of Virginia in 1967, a master’s degree in mathematics from Duke University in 1968, and a Ph.D. in computer science from Cornell in 1976.
Mr. Clarke was the former editor-in-chief of the journal Formal Methods in Systems Design and was one of the founders of the Computer Aided Verification conference.
“Intellectual rigor was a hallmark of Ed Clarke; it earned him computer science's highest honor and through him infused the computer science department for more than 30 years,” Martial Hebert, dean of CMU’s School of Computer Science, said in a statement. “He was a shining example for both the faculty and students and he is missed by all of us.”
He is survived by his wife, Martha, the graduate admissions coordinator for the Computer Science Department and School of Computer Science until her 2014 retirement. He also is survived by three sons, James Clarke of Portland, Ore.; Jonathan Clarke of Decatur, Ga., and Dr. Jeffrey Clarke of Durham, N.C.; and six grandchildren.
Private funeral services are being arranged by Laughlin Memorial Chapel in Mt. Lebanon. Contributions may be made to the Mt. Lebanon United Methodist Church Food Pantry, 3319 West Liberty Ave., Pittsburgh, PA 15216, and to the Edmund and Martha Clarke Endowed Graduate Fellowship in the School of Computer Science.
Andrew Goldstein: agoldstein@post-gazette.com.
First Published: December 24, 2020, 1:31 a.m.
Updated: December 24, 2020, 10:51 a.m.