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.
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
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
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.
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.