I will show how Parameterized Unit Tests (PUTs), a generalization of traditional unit tests, can be leveraged for systematic testing. PUTs are algebraic specifications written as code, describing the behavior of a program from a client's point of view. Traditional test cases can be obtained by supplying test inputs. Pex is a white box test input generation tool which analyzes the code of PUTs together with the program-under-test to determine relevant test inputs fully automatically. To this end, Pex performs dynamic symbolic execution, where the program is executed multiple times with different inputs while the taken execution paths are monitored. An SMT-solver with model-generation capabilities computes new test inputs that will exercise different execution paths. As a side effect of the analysis, Pex exposes bugs. The result is a traditional unit test suite with high code coverage. Pex has been used in Microsoft to test core .NET components. Pex is integrated in Visual Studio, and publicly available as an MSDN DevLabs project.

Nikolai Tillmann is a Principal Research Software Design Engineer at Microsoft Research. He is currently leading the Pex project - a white box test generation framework for .NET applications based on parameterized unit testing, dynamic symbolic execution, an SMT solver, and an integrated development and testing experience in Visual Studio. Previously he worked on AsmL, an executable modeling language, and Spec Explorer, a model-based testing tool. His research interests include program specification, analysis, testing, and verification. He received his M.S. (Diplom) in Computer Science from the Technical University of Berlin in 2000.