For their groundbreaking work in quality assurance processes, Carnegie Mellon's Edmund M. Clarke and two of his colleagues were awarded the prestigious A.M. Turing Award by the Association for Computing Machinery (ACM). The award is often called the Nobel of computing.
Known as "model checking," the innovative technique enables computer hardware and software engineers to efficiently locate errors in complex system designs.
"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."
Clarke shares this year's award with E. Allen Emerson of the University of Texas and Josef Sifakis of the University of Grenoble in France. Working with Emerson, Clarke conceived the original idea and developed the theory of model checking in 1981. Simultaneously, Sifakis conceived similar ideas independently. Clarke has continued to pursue model checking as his major research focus, transforming the theoretical ideas into a highly effective technology.
Their approach has helped designers and manufacturers to address verification problems and gain mathematical confidence that complex computer systems meet their specifications. Model checking is now the most widely used verification method in the hardware and software industries, according to the ACM.
Named for British mathematician Alan M. Turing, the award includes a $250,000 prize with financial support from Intel Corporation and Google, Inc.
Clarke is the FORE Systems Professor of Computer Science and a professor of electrical and computer engineering at Carnegie Mellon. Previous Turing Award winners from Carnegie Mellon include Alan J. Perlis, Dana Scott, Manuel Blum, Raj Reddy with Edward Feigenbaum, and Allen Newell with Herbert A. Simon.