Carnegie Mellon University professor Edmund M. Clarke has won the 2007 Turing Award, the prestigious Nobel Prize of computing, for his groundbreaking work to detect design errors in computer chips.
His pioneering 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 computer chips, systems and networks.
Clarke, the FORE Systems Professor of Computer Science, shares the award and the $250,000 prize with two computer scientists, E. Allen Emerson, a former student now at the
University of Texas at Austin, and Joseph Sifakis who worked independently at the
University of Grenoble in France.
Clarke and Emerson originated the idea of Model Checking at
Harvard in 1981 as a way to check for logic errors in computer circuitry and systems. Prior to Model Checking, these errors were approached on a “hit or miss” basis and often went undetected until after a product’s release, which resulted in costly corrections. Model Checking analyzes the logic underlying a design similar how to a mathematician’s uses a proof to determine that a theorem is correct.
“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 CMU’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.”
Writer:
Deb SmitSource: Byron Spice, Carnegie Mellon University
Image courtesy Carnegie Mellon University