| |||||||||||||
excessive focus on Engler's groupexcessive focus on Engler's groupPosted Nov 27, 2006 7:43 UTC (Mon) by JoeBuck (subscriber, #2330)Parent article: KHB: Automating bug hunting Dawson Engler and group are brilliant, and Coverity is a useful tool, but there's a hell of a lot of other useful research out there. While I'm normally the last to say anything good about Microsoft, their SLAM project is scary-impressive, and they've snapped up a lot of world-class formal verification researchers to work on it. Their device driver checkers appear to be more powerful and rigorous than Coverity's in that they yield proofs (not that there are no bugs, but that a whole series of properties are always satisfied on all code paths). And now they are making their tools available to Windows driver writers outside Microsoft. Also, many techniques that Valerie appears to credit Engler's group for actually originated in the hardware verification world, particularly symbolic simulation, hybrid symbolic/concrete state space exploration and constraint solving to create testcases with desired properties. But this is to be expected, because the standard for hardware perfection is much higher, and bugs can be much more costly (after Intel lost $470 million on the Pentium bug, they started spending a hell of a lot more money on advanced formal verification techniques).
(Log in to post comments)
|
|||||||||||||