Drive and monitor program executions to find bugs, using blackbox or whitebox techniques, random or systematic exploration, concrete or symbolic execution, etc.
|
Do you control your code? Pex puts you back into the driver’s seat. Right from the Visual Studio code editor, Pex finds interesting input-output values of your methods, which you can save as a small test suite with high code coverage. Pex performs a systematic analysis, hunting for boundary conditions, exceptions and assertion failures. Pex enables Parameterized Unit Testing, an extension of Unit Testing. |
|
|
CHESS is an automated tool for finding errors in multithreaded software by systematic exploration of thread schedules. It finds errors, such as data-races, deadlocks, hangs, and data-corruption induced access violations, that are extremely hard to find with current testing tools. CHESS will be shown at PDC 2008. |
|
|
We are conducting research on automating software testing using (static and dynamic) program analysis with the goal of building testing tools that are automatic, scalable and check many properties. Our work combines program analysis, testing, model checking and theorem proving. Examples of projects using our technology are Pex (see above) and SAGE. SAGE is a whitebox fuzzer for security testing, available only inside Microsoft. |
|
|
NModel is a model-based analysis and conformance testing framework for model programs written in C#. |
|
|
NinjaWare is a project investigating lightweight continuous monitoring and analysis of software. Our implementation allows us to gather fine-grain temporal information about high frequency events such as program data accesses with very low overhead (< 5%). We are exploring leveraging this infrastructure to build a wide variety of always-on runtime tools ranging from memory leak and data race detectors to program specification/invariant checkers and security monitors. |
|
|
PPP is a novel scheme for efficiently profiling paths in programs. We are investigating the use of PPP in residual path profiling, which seeks to identify all paths executed by deployed software that were untested during software development. |
|
|
Stubs is a lightweight stub framework for .NET that is enterily based on delegates, type safe, refactorable and source code generated. Stubs was designed support the Code Contracts runtime writter and provide a minimal overhead to the Pex white box analysis. |
|
Thomas Ball, Sebastian Burckhardt, Trishul Chilimbi, Peli de Halleux, Patrice Godefroid, Madan Musuvathi, Shaz Qadeer, Wolfram Schulte, Nikolai Tillmann, Margus Veanes.
|
Spec Explorer is a software development tool for advanced model-based specification and conformance testing. |
|
