MSDN Webcast: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods Inside Microsoft (Level 300)  

The SLAM project originated in Microsoft Research in early 2000. Its goal is to automatically check that a C program correctly uses the interface to an external library. The SLAM analysis engine forms the core of a new tool called Static Driver Verifier (SDV) that systematically analyzes the source code of Microsoft Windows device drivers against a set of rules that define what it means for a device driver to properly interact with the Windows operating system kernel. Join this webcast and learn about the history and inner workings of this innovative project, and see how it uses and extends ideas from symbolic model checking, program analysis and theorem proving in novel ways to address this problem.