[IGSTK-Developers] Dr. Dobb's | 2007 Turing Award Winners Announced | February 4, 2008

[Luis Ibanez]

http://www.ddj.com/206103622

2007 Turing Award Winners Announced
For their groundbreaking work on Model Checking
Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis are the
recipients of the 2007 A.M. Turing Award for their 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.

Clarke, a professor at Carnegie Mellon University, Emerson, of the
University of Texas, Austin, and Joseph Sifakis of the University of
Grenoble, will share $250,000. The Turing Award, presented annually by
the Association for Computing Machinery, 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

Model Checking 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.
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. Numerous model checking systems have been implemented,
such as Spin at Bell Labs.

Clarke implemented the first Model Checker in 1982. 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 CMU.