Overview

The Program Analysis research group is focused on the practical issue of helping Microsoft product groups develop better software. At the same time, our work has advanced the state of the art in the field of program analysis.

Our goal is to use program analysis technology to build tools for validating industrial-sized software. Validation tools require complete analysis of all execution paths. Unfortunately, complete program analysis methods exhibit a natural trade-off between precision and scalability. Our research deals with overcoming this tradeoff.

Over the last few years we have invented methods for scalable symbolic evaluation, scalable memory alias analysis, scalable call-graph construction, scalable value-flow analysis, and scalable dataflow analysis. Along the way we have built (and in some cases made available to the research community) infrastructures for scalable program analysis.

We believe in three fundamental techniques for developing software validation tools that scale to large programs. The first technique is to develop detailed global analyses that operate on a limited set of carefully chosen execution paths. The second technique is to develop approximate global analyses that sacrifice a small amount of precision for a large amount of scalability. The third technique is to combine interface-level source code annotations provided by the programmer with strong local analyses.

These three approaches are embodied in the projects we work on. All of our tools are run routinely over millions of lines of production quality commercial code.