Professor 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 Edmund 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", stated 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 programmes 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 analyses 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", stated 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 programmes that actually work as specified."
Edmund Clarke and E. Allen 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 Professor Clarke joined Carnegie Mellon in 1982, he implemented the first Model Checker. It could analyse 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, Professor 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 analyse 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", stated Randal E. Bryant, dean of the Carnegie Mellon School of Computer Science.
During the same time period, Joseph Sifakis also continued to work on Model Checking, extending the approach to address verification of real-time systems.
Professor Clarke has served on the editorial boards of numerous journals and is the former editor-in-chief ofFormal Methods in Systems Design. He is a co-founder, with Joseph 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.
Professor 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.