Wolfram Schulte, Microsoft Research
Nikolai Tillmann, Microsoft Research
Peli de Halleux, Microsoft Research
Pex supports test-driven development. From parameterized unit test, which define the requirements of the code to be developed, and the code, Pex automatically produces traditional unit tests cases with high code coverage. Moreover, when a generated test fails, Pex can often suggest a bug fix.
Pex monitors test execution and records detailed traces. From those traces, Pex learns the program behavior. It uses a constraint solver to perform a systematic program analysis, and by changing constraints it produces new test cases with different behavior.
In these lectures we introduce PEX, discuss its foundation, its limitations and apply it on real code. For information about Pex, see http://research.microsoft.com/Pex/.