The Association for Computing Machinery has announced the winners of the 2007 version of its prestigious Turing Award. Edmund M. Clarke of Carnegie Mellon, E. Allen Emerson of the University of Texas at Austin, and Joseph Sifakis of the University of Grenoble will share the prize for their work in developing a technique called model checking. Model checking tools automate the validation of software and hardware designs, and are heavily used in the commercial sector.
Model checking is a way of catching design flaws early in the process. Given an appropriately formatted specification for a product, model checking tools are able to determine whether a given design meets that specification. The three winners have been cited for just about everything involved with the field: establishing it during the early '80s, developing algorithms that led to practical applications, and expanding the scope of problems it can be applied to. Model checking is now used during the design process of processors, communication protocols, and real time systems.
The wide use of the technique is not a result of its ease or simplicity. Formally, it can only be applied to systems with a finite number of states, but in practice, many systems suffer from what's called "state explosion," where the number of possible states to be checked can't be handled by existing computers. The process itself can be unwieldy, as both the initial specification and the paths among possible states have to be described through structured, formalized code; you can get a sense of the challenges at this page.
Despite these challenges, the technique has some clear advantages, in that it not only catches errors prior to implementation, but also identifies the precise circumstances in which they fail. As such, it has been heavily adopted in hardware design (as hardware has a finite number of states) and for safety-critical systems.
In addition to the prestige, the award comes with a $250,000 cash prize provided by Google and Intel.
- Eurekalert: "Carnegie Mellon's Edmund M. Clarke wins A.M. Turing Award, computing's highest honor" (press release)