Colloquium Details
Pex: Dynamic Analysis and Test Generation for .NET
| Author: | Nikolai Tillmann Microsoft Research |
|---|---|
| Date: | June 28, 2007 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
| Host: | Yannis Smaragdakis |
Abstract
Pex (Program EXploration) is a test generation tool for .NET programs. Pex systematically enumerates feasible execution paths of the program-under-test using a technique based on Directed Automated Random Testing (DART). In this variant of symbolic execution, the program is executed repeatedly, initially with random inputs. The taken execution path is monitored and a symbolic representation of the path condition is obtained. The negation of the path condition gives rise to more execution paths using a constraint solver. The result of this process is a small test suite with high code coverage.
When a test fails, Pex determines likely root causes by tracing the data-flow across the abstraction boundaries present in .NET programs. Pex suggests the addition of missing precondition- and invariant validation code which will prevent the same failure from happening again.
Pex has been applied to code developed at Microsoft, and it has found previously unknown bugs in shipped and unshipped products.
Biography
Nikolai Tillmann has been with Microsoft Research since 2002. He develops modeling and testing tools in the group Foundations of Software Engineering. His current research is focused on dynamic and symbolic analysis of .NET programs (the Pex project). He received his M.S. (Diplom) in Computer Science from the Technical University of Berlin in Germany in 2000.