Microsoft Research
Microsoft Translator |
Pex and Moles - Publications

Also take a look at other projects and papers that use or extend Pex, and papers relating to Pex4Fun.

Overview Papers

Jonathan de Halleux and Nikolai Tillmann, Moles: tool-assisted environment isolation with closures, in TOOLS'10, Springer Verlag, July 2010

Isolating test cases from environment dependencies is often desirable, as it increases test reliability and reduces test execution time. However, code that calls non-virtual methods or consumes sealed classes is often impossible to test in isolation. Moles is a new lightweight framework which addresses this problem. For any .NET method, Moles allows test-code to provide alternative implementations, given as .NET delegates, for which C# provides very concise syntax while capturing local variables in a closure object. Using code instrumentation, the Moles framework will redirect calls to provided delegates instead of the original methods. The Moles framework is designed to work together with the dynamic symbolic execution tool Pex to enable automated test generation. In a case study, testing code programmed against the Microsoft SharePoint Foundation API, we achieved full code coverage while running tests in isolation without an actual SharePoint server. The Moles framework integrates with .NET and Visual Studio.

Nikolai Tillmann and Jonathan de Halleux, Pex - White Box Test Generation for .NET, in Proc. of Tests and Proofs (TAP'08), Springer Verlag, Prato, Italy, April 2008

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 path-bounded 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.

Key Papers describing Underlying Concepts

Nikolai Tillmann and Wolfram Schulte, Parameterized Unit Tests, in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, Inc., 2005

Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Parameterized unit tests separate two concerns: 1) They specify the external behavior of the involved methods for all possible test arguments. 2) Test cases can be re-obtained as traditional closed unit tests by instantiating the parameterized unit tests. Symbolic execution and constraint solving can be used to automatically choose a minimal set of inputs that exercise a parameterized unit test with respect to possible code paths of the implementation. In addition, parameterized unit tests can be used as symbolic summaries which allows symbolic execution to scale for arbitrary abstraction levels. We have developed a prototype tool which computes test cases from parameterized unit tests; it is integrated into the forthcoming Visual Studio Team System product. We report on its first use to test parts of the .NET base class library.

Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte, Fitness-Guided Path Exploration in Dynamic Symbolic Execution, in Proc. the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2009), IEEE, June 2009

Dynamic symbolic execution is a structural testing technique that systematically explores feasible paths of the program under test by running the program with different test inputs to improve code coverage. To address the space-explosion issue in path exploration, we propose a novel approach called Fitnex, a search strategy that uses state-dependent fitness values (computed through a fitness function) to guide path exploration. The fitness function measures how close an already discovered feasible path is to a particular test target (e.g., covering a not-yet-covered branch). Our new fitness-guided search strategy is integrated with other strategies that are effective for exploration problems where the fitness heuristic fails. We implemented the new approach in Pex, an automated structural testing tool developed at Microsoft Research. We evaluated our new approach by comparing it with existing search strategies. The empirical results show that our approach is effective since it consistently achieves high code coverage faster than existing search strategies.

All Publications related to Pex and Moles

    2013

    2012

    2011

    2010

    2009

    2008

    2007

    2006

    2005

    • Nikolai Tillmann and Wolfram Schulte, Parameterized Unit Tests with Unit Meister, in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, Inc., 2005
    • Nikolai Tillmann and Wolfram Schulte, Parameterized Unit Tests, in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, Inc., 2005