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.
11:00Paper Session
One - Research:Adequacy and Oracles Session Chair: Paul Strooper
12.30 Lunch
1:45 Walk
3:00 Tea
3.30Paper Session Two - Research and
Tools:Selection and Generation Session Chair: Michael Hennell
4:30Paper Session Three - Industry
Challenge and Experience Reports:Integration
Testing Session Chair: Marc Roper
5:30Paper Session Four - Research and
Experience Reports:Models and
Generation Session Chair: Anthony J H Simons
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.
10:00Paper Session Five - Research:Generation and Localization Session Chair: Bill Langdon
11:00 Coffee
11:30 Paper Session Six - Fast
Abstracts:Models and Oracles Session Chair: Gordon Fraser
12:30 Feedback Session for Fast Abstracts
Session Chair: Gordon Fraser
9:45Paper Session Eight -
Research:Economics and Effectiveness Session Chair: Daniel Hoffmann
10:45 Coffee
11:15Paper Session Nine - Research and
Experience:New Domains Session Chair: Neil Walkinshaw
12:15 Challenge Session: Connecting Theory and Practice
Session Chair: Leonardo Bottaci
1:00 Lunch
2:00Paper Session Ten -
Research:Testing and Security Session Chair: Harry Sneed
3:00 Tea
4:00 Closing Remarks and Next Steps
Presentation Details: Full papers have a twenty-five
minute presentation followed by five minutes of questions. Fast
abstracts have ten minutes for presentation and five minutes for
questions.