Dsc: Dynamic Symbolic Execution Engine for Java

Dsc is a dynamic symbolic execution engine and test case generator for Java (bytecode) programs.


Dsc is implemented in Java 6. Dsc uses Asm to instrument Java classes at load-time. Dsc uses the instrumentation code to build and maintain a symbolic shadow representation of the dynamic program state (call stack, operand stacks, and heap). To reason about the program and generate test cases for the program, Dsc uses the Z3 theorem prover from Microsoft Research. To communicate with Z3, Dsc uses a SWIG-generated Z3-wrapper.


Dsc is built on top of several third-party software components. For example, in the current release, Dsc uses the Z3 theorem prover from Microsoft Research. For your convenience, we distribute Dsc together with all third-party software components that are currently required to run Dsc. However, it is your responsibility to satisfy the license terms of each third-party software component. The following list is just for informational purposes and may be wrong. You are responsible for ensuring that you have the proper licenses.


Dsc is an academic prototype. Dsc has many known and unknown bugs. It is not integrated with any IDE. If you are looking for a related tool that is actually usable, we highly recommend Microsoft Pex.

Known limitations include the following. If the analyzed program uses one or more of these features, Dsc is in trouble.


Mock class generation

Some code under test refers to abstract types such as interfaces. If the abstract types are not implemented by any concrete classes (yet), the code cannot be executed. To address this problem, Dsc has a mock class generation extension, which reasons about type constraints and generates such required concrete classes. This even works for complex type constraints involving several abstract types and code under test that uses reflection to check type constraints.

The mock class generator also handles code under test that uses reflection to check for annotations.

Primary contact: Mainul Islam.

Dumper mode: Using Dsc without the platform-dependent Z3 constraint solver

Dsc derives much of its power from the excellent Z3 constraint solver from Microsoft Research. However, for some applications of Dsc, a constraint solver is not needed. For example, the CarFast project uses Dsc to just collect and emit symbolic constraints. CarFast then uses its own solvers to reason about these constraints.

To support such uses of Dsc, Dsc has a "dumper mode", which just dumps collected constraints to disk. In this mode, Dsc can be invoked without the Z3 binaries being present. This should allow Dsc to be used on any platform. To invoke Dsc in dumper mode, use the following configuration option:


Primary contact: Ishtiaque Hussain.



The Dsc configuration page contains basic hints on how to run and configure Dsc.


Besides this page and the configuration page, there is no documentation yet.

Technical Talks

Testing, reverse engineering, data structure repair, etc., via Dynamic Symbolic Execution
Microsoft Research Faculty Summit 2010 in Redmond, Washington on Monday, July 12, 2010 [slides]

Publications on Dsc

Dsc+Mock: A test case + mock class generator in support of coding against interfaces (Proc. 8th International Workshop on Dynamic Analysis (WODA), 2010)
Dsc+Mock is a dynamic symbolic test case generator that can reason about type constraints and can generate mock classes that satisfy such constraints. Our prototype implementation achieved higher code coverage than related test case generators that do not generate mock classes, such as Pex.

Publications on Dsc Applications

Data-Structure Repair

DSDSR: A tool that uses dynamic symbolic execution for data structure repair (Proc. 8th International Workshop on Dynamic Analysis (WODA), 2010)
This paper discusses the implementation of our dynamic symbolic data structure repair tool, DSDSR. We provide initial empirical results of applying DSDSR on different formulations of the same correctness condition and compare DSDSR with a state-of-the-art tool, Juzi.
Dynamic symbolic data structure repair (Proc. 32nd ACM/IEEE International Conference on Software Engineering (ICSE), Volume 2, Emerging Results Track, 2010)
We motivate how dynamic symbolic techniques enable generic repair to support a wider range of correctness conditions and present DSDSR, a novel repair algorithm based on dynamic symbolic execution. We implement the algorithm for Java and report initial empirical results to demonstrate the promise of our approach for generic repair.


CarFast: Achieving higher statement coverage faster (Proc. 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2012)
For a given branching statement encountered during program execution, CarFast estimates the number of statements that are yet uncovered but reachable from the respective branch outcomes. With the symbolic path condition collected during execution, CarFast selects input values such that a future execution will trigger a branch (path) that contains a high number of those yet uncovered statements.
New Ideas Track: Testing MapReduce-style programs (Proc. 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), New Ideas Track, 2011)
We formalize a MapReduce-specific correctness condition that all MapReduce applications have to satisfy, in order to be free of a certain class of bugs. To detect such bugs, we then design a technique that encodes the correctness condition as symbolic program constraints, checks them via dynamic symbolic execution, and generates corresponding test cases.
Is data privacy always good for software testing? (Proc. 21st IEEE International Symposium on Software Reliability Engineering (ISSRE), 2010)
Software testing interacts with data anonymization in surprising ways. I.e., increasing data anonymity to protect data during testing can drastically decrease test coverage. One problem is that current anonymization techniques do not take into account how the application under test actually uses the data. We therefore propose to guide data anonymization techniques with program analysis. Received the Best Paper Award.
Dynamic symbolic database application testing (3rd International Workshop on Testing Database Systems (DBTest), 2010)
We use dynamic symbolic execution to obtain a program path-condition. We then use this path-condition as a database query.


This material is based upon work supported by the National Science Foundation under Grants No. 1017305 and 1117369. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Additional financial support for the Dsc project has been provided by the University of Texas at Arlington.


The following people have checked into the current Dsc repository code or other documents.


Christoph Csallner, Ishtiaque Hussain, Mainul Islam, SERC lab in the Computer Science and Engineering Department at the University of Texas at Arlington

This Website

This website was updated on 13 September 2013 with bibtex2web.