Abstract: The Windows division of Microsoft Corporation is in the midst of a massive effort to improve the security and reliability of the next release of the product—Windows Vista. In this talk, I will explain how the Center for Software Excellence at Microsoft has used program verification technology to build the tools that enable this effort. Along the way, I will cover the current Windows engineering process and the role of the tools in the process, the core program verification techniques we have invented and used in the tools, business and environment issues that govern the engineering process, and research directions suggested by our experience so far.

Manuvir Das leads the Program Analysis research group in the Center for Software Excellence at Microsoft Corporation, and is an affiliate faculty member at the University of Washington. His research interests are in inventing and applying techniques from Programming Languages, Compilers, and Systems to the software engineering process. Manuvir holds a bachelor's degree in Computer Science from IIT Bombay, and a PhD in Computer Science from the University of Wisconsin-Madison.