2008 Turing Award Winners Announced

The Association for Computing Machinery has announced the 2008 Turing Award Winners. Edmund M. Clarke, Allen Emerson, and Joseph Sifakis received the award for their work on an automated method for finding design errors in computer hardware and software. "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."

Comments

WARNING: GNAA

[SirBudgington]

Link is a malicious site, don't click. Shock site with malicious jacascript.

Re:WARNING: GNAA

[Anonymous Coward]

Am I the only one who noticed that these are the winners from last year? Mod please?

Primary Source

[jdschulteis]

At least DDJ isn't somebody's blog, but why not link directly to ACM's press release?

VIS - An open source model checker

[b0101101001010000]

Fabio Somenzi at the University of Colorado contributes to an open source tool to perform model checking called VIS (Verification Interacting with Synthesis) available at: http://vlsi.colorado.edu/~vis/. I recommend anyone interested in this to check it out. It can perform model checking on Verilog modules directly.

Re:Just moves the errors up one level

[Picolino]

The purpose of model checking is rarely to specify the whole behavior of the program, but to ensure that some condition are always true or false. Such condition can be the absence of buffer overflow ... relatively easy to formulate, hard to discover ...

Re:Guarding the guard

[El Cabri]

You're not expected to model the full behavior of your program. Model checking is useful for testing individual properties such as bounds on ressource allocation, non-deadlock of thread synchronization, or security-related invariants.

An open source model checker for Java

[martinde]

NASA released an open source model checker for Java called JPF. It's a JVM implemented in Java that can do model checking on "generic" Java apps, finding deadlocks and things like that.

Just about time

[leoval]

I have been hearing about formal verification for hardware design for the last 10 years and at some point I had to opportunity to do minor work on one of the formal verification products that my company produces. The technology is really interesting and contrary the the uninformed opinion of other slashdotters in this thread, it delivers tangible results and provides a clear advantage over classic verification techniques (vector testing, testbenches and so for).

It took a long time but a lot of the major design houses (Intel, PMC sierra, Freescale, ST micro, IBM and such), now use a form or another of formal verification during their design cycle. It has been a silent revolution, but be assured that many modern microchips have been verified this way.

Perhaps some day we could have a succesful formal verification product for software (After all, Verilog and VHDL could be seen as programming languages no?). In the meantime, it has proven its worth on the hardware side. Congratulations are due to these pioneers.

Re:Just moves the errors up one level

[Coryoth]

The program became little more than a different expression of the formal specifications, such that it would be possible not only to check that a program had no "errors" and followed the specification exactly, but it would also be possible to have an automated process translate the formal specification into a program directly. That depends on the problem. I can specify a square root finding algorithm: the output multiplied by itself must be equal to the input (within some epsilon error tolerance). I doubt you can extract any useful implementation from that. A slightly more complicated example, I can specify a sorting algorithm: the output must have all the same elements as the input, and for each index i of the ouput the ith element must be less than the (i+1)th element. Trying to translate that (or its more formal equivalent) into a program directly will get you bogosort at best. Specification can be, and usually are, considerably shorter than implementations; this is particularly true wen you start specifying code that is more than just a set of business rules.