image: Carnegie Mellon University computer science professor Edmund M. Clarke and two other computer scientists will receive the 2007 A.M. Turing Award from the Association for Computing Machinery. view more
Credit: Carnegie Mellon University
PITTSBURGH— Carnegie Mellon University Computer Science Professor Edmund M. Clarke and two computer scientists from the University of Texas at Austin and the University of Grenoble in France, are winners of the 2007 A.M. Turing Award in recognition of their pioneering work on an automated method for finding design errors in computer hardware and software.
The method, called Model Checking, is the most widely used technique for detecting and diagnosing errors in complex hardware and software design. It has helped to improve the reliability of complex computer chips, systems and networks.
The Turing Award, presented annually by the Association for Computing Machinery (ACM), is considered to be the most prestigious award in computing. Often referred to as “the Nobel Prize of computing,” it is named for British mathematician Alan M. Turing.
Clarke, the FORE Systems Professor of Computer Science and professor of electrical and computer engineering, will share the award and its $250,000 prize with E. Allen Emerson, who worked with Clarke in developing Model Checking as his graduate student at Harvard University and later as a professor at the University of Texas at Austin. Also sharing the award is Joseph Sifakis who, working independently, developed a similar technique at the Centre National de la Recherche Scientifique at the University of Grenoble.
“We at Carnegie Mellon take pride in solving real-world problems and few projects exemplify that quality better than Ed Clarke’s work on Model Checking,” said Carnegie Mellon President Jared L. Cohon. “Reliability has become critical as computer technology has grown in both complexity and ubiquity. Model Checking gives us confidence that these machines will do what we expect and need them to do.”
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 computer chips grew to include hundreds of thousands or millions of transistors, and as software and computer systems similarly grew in complexity, these hit-or-miss “informal verification” methods became inadequate to the task. 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.
“The influence of Model Checking on both theory and practice has been tremendous, but the full impact is still ahead of us,” said Peter Lee, professor and head of Carnegie Mellon’s Computer Science Department. “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.”
Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem.
When Clarke joined Carnegie Mellon in 1982, he implemented the first Model Checker. It could analyze all the possible states of a given circuit, but was limited to relatively small designs — much smaller than the systems being built by computer manufacturers.
In 1987, Clarke’s graduate student, Kenneth McMillan, realized that he could implement Model Checking by a series of operations on binary decision diagrams (BDDs), a method of representing symbolic information that had recently been developed by another Carnegie Mellon computer science professor, Randal E. Bryant. This new system, called Symbolic Model Checking, was able to analyze billions of billions of states, making it relevant to commercial computer design problems and leading to its widespread adoption by the industry. For this invention, Bryant, Clarke, Emerson and McMillan won the 1998 Paris Kanellakis Award for Theory and Practice from the ACM. In 1999, they also received the Allen Newell Award for Research Excellence from Carnegie Mellon.
“Ed Clarke and his students have been able to apply abstract logical theories to the real-world problem of making sure our computer systems will really work. His work has been very influential on mine, and I consider it a privilege to have served and worked with him at Carnegie Mellon,” said Bryant, dean of the Carnegie Mellon School of Computer Science.
During the same time period, Sifakis also continued to work on Model Checking, extending the approach to address verification of real-time systems.
Clarke has served on the editorial boards of numerous journals and is the former editor-in-chief of Formal Methods in Systems Design. He is a co-founder, with Sifakis, Robert Kushan and Amir Pnueli, of the annual International Conference on Computer-Aided Verification (CAV), which since 1989 has served as the major forum for research in the field of formal verification. He received a Technical Excellence Award from the Semiconductor Research Corporation in 1995, and the Institute of Electrical and Electronic Engineers (IEEE) Harry M. Goode Memorial Award in 2004. He is a Fellow of both the ACM and the IEEE, and was elected to the National Academy of Engineering in 2005.
Clarke received a bachelor’s degree in mathematics from the University of Virginia and a master’s degree in mathematics from Duke University. He earned a Ph.D. in computer science from Cornell University, and has taught at Harvard and Duke.
Three additional current and emeritus faculty members from Carnegie Mellon have won the Turing Award: Dana Scott in 1976, Raj Reddy in 1994 and Manuel Blum in 1995. Of the 51 recipients of the award in its 42-year history, 10 have been affiliated at some time with Carnegie Mellon as either students or faculty. The ACM will present the 2007 award at the annual ACM Awards Banquet on June 21, 2008, in San Francisco.
About Carnegie Mellon: Carnegie Mellon is a private research university with a distinctive mix of programs in engineering, computer science, robotics, business, public policy, fine arts and the humanities. More than 10,000 undergraduate and graduate students receive an education characterized by its focus on creating and implementing solutions for real problems, interdisciplinary collaboration, and innovation. A small student-to-faculty ratio provides an opportunity for close interaction between students and professors. While technology is pervasive on its 144-acre Pittsburgh campus, Carnegie Mellon is also distinctive among leading research universities for the world-renowned programs in its College of Fine Arts. A global university, Carnegie Mellon has campuses in Silicon Valley, Calif., and Qatar, and programs in Asia, Australia and Europe. For more, see www.cmu.edu.