Parameterized Unit Testing with Pex: Automated White Box Testing for .NET

Abstract

I will talk about how automated program analysis techniques can be combined with unit testing to develop more thoroughly tested code in less time. First, the developer writes Parameterized Unit Tests (PUTs) instead of traditional unit tests. PUTs are algebraic specifications written as code, describing the behavior of a program from a client's point of view. Then Pex, an incubation project for Visual Studio developed at Microsoft Research, analyzes the PUTs together with the code under test. Pex computes test inputs that will trigger different program behaviors. The result is a traditional test suite that often achieves high code coverage and may expose bugs. To this end, Pex performs dynamic symbolic execution, where the program is executed multiple times with different concrete inputs, while the taken execution paths are monitored at the instruction level. A constraint solver computes new concrete test inputs that will exercise different execution paths. Pex has been used in Microsoft to test core .NET components. Pex is publicly available, enabling a new software development and testing experience.

Biography

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.

Property Based Testing with QuickCheck

Abstract

QuickCheck is a random testing tool which tests programs against formal specifications expressed in a functional programming language, reducing failing tests to minimal counterexamples from which errors can easily be diagnosed. We use functional programming both as a tool for modeling the system under test, and as a meta-language in which domain specific testing languages can easily be embedded. In this talk, I will demonstrate the QuickCheck tool itself and the property-driven development style it supports, describe some industrial applications, and present some recent results in state-machine testing and specification generation from the FP7 project ProTest.

Biography

John is a well-known researcher in the area of functional programming and is the author of more than 50 research papers. He was appointed to a Chair at the age of 27 by the University of Glasgow, and since 1992 has held a Chair in Computer Science at Chalmers University, Gothenburg. He now divides his time between Chalmers and QuviQ AB, a company that he founded with Thomas Arts in May 2006.