In addition to Prefast, there is also the Static Driver Verifier(SDV). Comes with the Windows Driver Kit, analyzes your code to detect common problems people ha

In addition to Prefast, there is also the Static Driver Verifier(SDV). Comes with the Windows Driver Kit, analyzes your code to detect common problems people have when writing drivers. The Windows Driver Kit is free -- you can learn more about SDV here: http://www.microsoft.com/whdc/devtools/tools/sdv.mspx http://www.microsoft.com/whdc/devtools/tools/sdv.mspx SDV began its life as a project called SLAM. This page has documentation on SLAM, academic papers, etc. http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/ I'm not sure of the exact connection highlighted in the article, but this work builds on decades of work in automated theorem proving. It's exciting that now these techniques are used on real code. (Disclosure: the SLAM & SDV authors are colleagues of mine at Microsoft.)