UTCS Colloquium: Nikolai Tillmann/Microsoft Research:Parameterized Unit Testing with Pex a White Box Test Input Generation Tool for .NET ACES 2.402 Wednesday November 5 2008 3:00 p.m.

Contact Name: 
Jenna Whitney
Nov 5, 2008 3:00pm - 4:00pm

There is a signup schedule for this event (UT EID required).
Type of Talk: UTCS Colloquium

Speaker/Affiliation: Nikolai Tillm

ann/Microsoft Research

Date/Time: Wednesday November 5 2008 3:00

Location: ACES 2.402

Host: Jim Browne

Talk Tit

Parameterized Unit Testing with Pex a White Box
Test Input Gene

ration Tool for .NET

Talk Abstract:
Parameterized Unit Tests (PUT

s) are a generalization
of traditional unit tests. PUTs are algebraic s

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 too

l for .NET. Pex analyzes the code
of PUTs together with the program-und

er-test to determine
relevant test inputs fully automatically. To this

end Pex uses
dynamic symbolic execution where the program is executed

multiple times with different inputs while the taken execution

hs are monitored. An SMT-solver with model-generation
capabilities comp

utes new test inputs that will exercise
different execution paths. As a
side effect of the analysis
Pex exposes bugs. The result is a traditi

onal unit test suite
with high code coverage. Pex is integrated in Visu

al Studio.

Speaker Bio:
Nikolai Tillmann is a Principal Research
Software Design
Engineer at Microsoft Research. He is currently leadin

the Pex project a framework for runtime verification and

c test case generation for .NET applications based
on parameterized uni

t testing dynamic symbolic execution
and an SMT solver. Previously h

e worked on AsmL an
executable modeling language and Spec Explorer a
based testing tool. His research interests include program

pecification analysis testing and verification. He received
his M.S.
(Diplom) in Computer Science from the Technical
University of Berlin i

n 2000.