Microsoft's Secret Bug Squasher
It turns out that a good portion of all those Windows crashes over the years are not caused by the operating system itself, but by buggy device drivers -- low-level pieces of code that allow the operating system to communicate with external devices like the computer's keyboard, hard drive, screens and network cards.
Because device drivers run deep within the operating system, they are hard to write and hard to debug. And when they fail, they can take down the whole computer. "If they go bad, the whole OS can go bad," says Tom Ball, a scientist at Microsoft Research. But in a little-noticed project percolating in Redmond, the world's biggest single producer of software bugs is pushing the envelope on an anti-bug technology that promises to make the Windows operating system a whole lot more reliable, and may eventually raise the bar for dependable software throughout the industry.
Microsoft has developed a tool called the Static Driver Verifier, or SDV, that uses "model checking" to analyze the source code for Windows device drivers and see if the code that the programmer wrote matches a mathematical model of what a Windows device driver should actually do. If the driver doesn't match the model, the SDV warns that the driver might contain a bug.
