When Edmund M. Clarke figured out in 1981 how to detect design errors in computer chips, hardware and software, he experienced not only the thrill of discovery but also expectations that it could solve major problems for the computer world.
At long last, he's being recognized for his accomplishments.
Dr. Clarke, the FORE Systems Professor of Computer Science at Carnegie Mellon University, is one of three winners of the Turing Award, recognized as the Nobel Prize for computing.
"It's very gratifying knowing that something I came up with 26 years ago, and have been working on ever since, has become a useful technique," Dr. Clarke said. "But I still would say that the first research I did on this, and the realization it would be something important, was more rewarding."
Dr. Clarke will share the $250,000 prize with E. Allen Emerson, his former student and now a research collaborator at the University of Texas at Austin, and Joseph Sifakis, who worked independently at the University of Grenoble in France.
The Turing Award, which the Association for Computing Machinery presents annually, is considered the most prestigious award in computing. It is named in honor of British mathematician Alan M. Turing.
Dr. Clarke said he and Carnegie Mellon colleagues celebrated the award yesterday morning with a glass of champagne. Receptions in his honor were held throughout the day at the university.
Dr. Clarke's honor reflects his pioneering work in model checking -- a system that uses computer logic to check for errors in complex computer chips, systems and networks. The method of testing and outlining errors has become integral to the design of such systems.
Although Dr. Clarke and Dr. Emerson, then a student, originated the idea of model checking at Harvard University, Dr. Clarke's 1982 move to Carnegie Mellon, where he built his first model checker, represented an important step in its development.
"Here you can come up with theoretical insights and be encouraged to come up with practical applications," he said in praise of Carnegie Mellon's computer science department.
A 1999 Pittsburgh Post-Gazette article described the importance of model checking: In 1994, Intel had introduced its Pentium microprocessor, but an error in the computer chip's ability to divide large numbers was discovered later. Although not a major flaw, it cost Intel about $500 million to fix it.
Dr. Clarke's method makes sure software and chips contain no logical lapses in circuitry or programming. It considers every possible state of a hardware or software design and determines if the circuitry meets the designer's specifications, and, if not, how best to debug the errors.
Model checking has become the most widely used formal verification technique for detecting and diagnosing design errors in hardware and software. Dr. Clarke said Intel, IBM and Microsoft, among others, regularly use it to make chips, systems and networks more reliable.
In a news release, professor Peter Lee, head of Carnegie Mellon's computer science department, said that model checking has had a tremendous influence on theory and practice, but its full impact lies ahead.
"Ideas based on model checking are getting us closer to new software development methods that may, for the first time, give us programs that actually work as specified," he said.
Three current or emeritus Carnegie Mellon faculty members have won the Turing Award. Dana Scott won it in 1976, Raj Reddy in 1994 and Manuel Blum in 1995. Ten of the 51 award recipients have been affiliated at some time with the university as students or faculty.
On June 21, the association will present its 2007 award during its annual banquet, this year in San Francisco.
First Published: February 5, 2008, 5:00 a.m.
