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.
Citation
Kasper Luckow,
Marko Dimjasevic,
Dimitra Giannakopoulou,
Falk Howar,
Malte Isberner,
Temesghen Kahsai,
Zvonimir Rakamaric,
Vishwanath Raman
JDart: A Dynamic Symbolic Analysis Framework
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 9636: 442--459, doi:10.1007/978-3-662-49674-9_26, 2016.
BibTeX
@inproceedings{2016_tacas_ldghikrr,
title = {JDart: A Dynamic Symbolic Analysis Framework},
author = {Kasper Luckow and Marko Dimjasevic and Dimitra Giannakopoulou and Falk Howar and Malte Isberner and Temesghen Kahsai and Zvonimir Rakamaric and Vishwanath Raman},
booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
series = {Lecture Notes in Computer Science},
volume = {9636},
publisher = {Springer},
editor = {Marsha Chechik and Jean-Fran{\c{c}}ois Raskin},
pages = {442--459},
doi = {10.1007/978-3-662-49674-9_26},
year = {2016}
}
Acknowledgements
Supported in part by NASA Contr. NNX14AI09G and NSF CCF 1421678/1422705.