Edmund Clarke Pioneered Methods for Detecting Software, Hardware Errors

CMU Professor Earned Turing Award, Computer Science's Highest Honor

Wednesday, December 23, 2020 - by Byron Spice

Edmund M. Clarke, University Professor Emeritus

Edmund M. Clarke, University Professor Emeritus at Carnegie Mellon University and co-recipient of the 2007 Turing Award – computer science's equivalent of the Nobel Prize – died Dec. 22 of COVID-19, following a long illness.

Clarke, together with his Harvard University graduate student, E. Allen Emerson, and, working separately, Joseph Sifakis of the University of Grenoble, developed an automated method for detecting design errors in computer hardware and software. Called model checking, it is widely used and has helped to improve the reliability of complex computer chips, systems and networks. The Association for Computing Machinery (ACM) awarded the Turing to the three scientists for this achievement.

"With Ed Clarke's passing, the world lost a giant in computer science and CMU said goodbye to a beloved member of our community," said Farnam Jahanian, president of Carnegie Mellon University. "Ed’s pioneering work in model checking applied formal computational methods to the ultimate challenge: computers checking their own correctness. 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.”

Since the dawn of computing, engineers have checked for logic errors in computer circuitry or software programs by running simulations to test performance and by manually checking each line of computer code. But as the number of components on computer chips grew geometrically and as software and computer systems similarly became more complex, these hit-or-miss "informal verification" methods proved inadequate. Errors often went undetected until after a product was released, when correcting even minor errors is expensive.

Model checking, by contrast, is a type of "formal verification" that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, model checking considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications.

"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," said Martial Hebert, dean of Carnegie Mellon's School of Computer Science. "He was a shining example for both the faculty and students and he is missed by all of us."

Clarke earned his Ph.D. in computer science at Cornell University in 1976. He taught at Duke University and then Harvard before joining CMU's Computer Science Department in 1982, where his research group continued to pioneer formal verification and automatic theorem proving. He is one of the founders of the Computer Aided Verification conference and was the former editor-in-chief of the journal Formal Methods in Systems Design.

He became an emeritus professor in 2015.

"Ed Clarke was a brilliant researcher but also a kind and caring individual," said Randal E. Bryant, Founders University Professor of Computer Science Emeritus. "I especially admire his ability to mentor Ph.D. students and postdoctoral researchers, many of whom have had major impact throughout the world through their research."

In 1995, Clarke was the first recipient of the endowed FORE Systems Professorship and in 2008 was named a University Professor, CMU's highest faculty honor. He is the co-recipient of the 1998 ACM Kanellakis Award, the 1999 Allen Newell Award for Excellence in Research, the 2004 IEEE Harry H. Goode Memorial Award and the Conference on Automated Deduction's 2008 Herbrand Award for Distinguished Contributions to Automated Reasoning. In 2014, the Franklin Institute presented him its Bower Award and Prize for Achievement in Science for his leading role in the conception and development of techniques for verification of computer systems.

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, Oregon; 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. The family requests contributions 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.

For more information, Contact:
Byron Spice | 412-268-9068 | bspice@cs.cmu.edu