Pex-White Box Test Generation for .NET

Pex automatically produces a small test suite with high code coverage for a .NET program. To this end, Pex performs a systematic program analysis (using dynamic symbolic execution, similar to pathbounded model-checking) to determine test inputs for Parameterized Unit Tests. Pex learns the program behavior by monitoring execution traces. Pex uses a constraint solver to produce new test inputs which exercise different program behavior. The result is an automatically generated small test suite which often achieves high code coverage. In one case study, we applied Pex to a core component of the .NET runtime which had already been extensively tested over several years. Pex found errors, including a serious issue. 1 Overview Pex [24] is an automatic white-box test generation tool for .NET. Starting from a method that takes parameters, Pex performs path-bounded model-checking by repeatedly executing the program and solving constraint systems to obtain inputs that will steer the program along ...

• Type: Journal
• Year: 2008
• Where: TAP
• Authors: Nikolai Tillmann, Jonathan de Halleux
• Keywords: Dynamic Symbolic Execution, Execution Paths, Hardware, Small Test Suite, TAP 2008