Microsoft's Secret Bug SquasherMicrosoft 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.
You can find the rest of the story
Here