Click Here to Install Silverlight*
United StatesChange|All Microsoft Sites
Center for Software Excellence 
Program Analysis Projects

We use program analysis technology to build tools for validating industrial-sized software. Validation tools require complete analysis of all execution paths. Program analysis methods require a trade-off between precision and scalability. We strive to overcome this tradeoff.

Please note that the key technical ideas behind these projects are under patent protection. Public information is available on these pages, and in our published papers listed below.

Current Projects

Error Detection via Scalable Program Analysis (ESP)

ESP provides a method for static (i.e., compile-time) detection of protocol errors in large C/C++ programs. Its input is a set of source files and a specification of a high-level protocol that the code in the source files is expected to satisfy. Its output is either a guarantee that the code satisfies the protocol along all execution paths, or a browsable list of execution traces that lead to violations of the protocol. We have recently used ESP to validate the Windows OS kernel against a category of security properties. This result raises the state of the art in terms of scalable program verification by an order of magnitude.

Annotation-based Software Validation (espX)

espX is a tool for compile-time buffer overrun detection. It is based on a combination of strong local checking and interface annotations added by programmers. Novel features of our approach are a restricted annotation language that reduces programmer effort, a technique for generating annotations automatically, and a validation algorithm that combines various forms of analysis.

Intra-procedural Source Code Analysis (PREfast)

A key factor in reducing the cost of software development is prevention of bugs from getting introduced into the product. PREfast helps address this problem by preventing developers from checking in code with certain classes of bugs. PREfast uses a mix of syntactic and semantic analysis to look for these bugs. PREfast also exposes an extensibility mechanism that lets different product groups enforce product specific coding conventions as part of the compilation process. PREfast is currently being used as a check-in requirement for most Microsoft product groups.

Scalable, Path Sensitive Source Code Analysis (PREfix)

PREfix is a tool used at compile-time to detect defects in C and C++ source code through symbolic evaluation techniques. PREfix automatically simulates the execution of source code components along a selected set of program paths and queries the execution state in order to identify programming errors, all without requiring test cases or instrumentation. PREfix includes a rich infrastructure for producing, displaying, managing, and ranking error messages. Because of this simulation process, PREfix can be used early in the development process - even before the program code is complete enough to fully execute. PREfix can also be used to effectively maintain existing code bases.

Efficient Local Analysis (PREsharp)

PREsharp is a defect detection tool for C#. It exposes compiler-generated ASTs to custom defect detection plug-ins, which walk the ASTs to perform local analysis. PREsharp is the counterpart in the C# world of PREfast, the AST-based defect detection tool for C/C++ developed by CSE.

Post Mortem Analysis (PSE)

PSE is a tool for post-mortem analysis of known program failures, described in an FSE 2004 paper. Its input is a set of source files and a specification of an error, including an error point and a partial stack dump. Its output is a browsable list of execution traces that result in the given error. The key component of PSE is a backwards analysis that tracks the flow of values in the opposite direction of program flow.

Previous Projects

Flow-Insensitive Alias Analysis. We previously developed two new algorithms for scalable alias analysis, both of which were described in PLDI 2000 papers. The algorithms take as input a set of source files, and produce memory alias information and call graphs that are complete in the presence of function pointers and calls to virtual methods.

Context-Sensitive Value Flow Analysis. We previously invented a new scalable algorithm for tracing the flow of values through a program in a context-sensitive manner. This algorithm, GOLF, has been described in papers at SAS 2001 and SAS 2002.


Program Analysis



Research Papers




© 2017 Microsoft Corporation. All rights reserved. Contact Us |Terms of Use |Trademarks |Privacy & Cookies