JDart: A dynamic symbolic analysis framework

Abstract

We describe JDART, a dynamic symbolic analysis framework for Java. A distinguishing feature of JDART is its modular architecture: the main component that performs dynamic exploration communicates with a component that efficiently constructs constraints and that interfaces with constraint solvers. These components can easily be extended or modified to support multiple constraint solvers or different exploration strategies. Moreover, JDART has been engineered for robustness, driven by the need to handle complex NASA software. These characteristics, together with its recent open sourcing, make JDART an ideal platform for research and experimentation. In the current release, JDART supports the CORAL, SMTInterpol, and Z3 solvers, and is able to handle NASA software with constraints containing bit operations, floating point arithmetic, and complex arithmetic operations (e.g., trigonometric and nonlinear). We illustrate how JDART has been used to support other analysis techniques, such as automated interface generation and testing of libraries. Finally, we demonstrate the versatility and effectiveness of JDART, and compare it with state-of-the-art dynamic or pure symbolic execution engines through an extensive experimental evaluation.