JDart: A Dynamic Symbolic Analysis Framework


Kasper Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, Vishwanath Raman. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, the Netherlands.
[pdf] [bib]

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.


  author = {Kasper Luckow and Marko Dimja\v{s}evi\'c and Dimitra Giannakopoulou and Falk Howar
    and Malte Isberner and Temesghen Kahsai and Zvonimir Rakamari\'c and Vishwanath Raman},
  title = {{JDart}: A Dynamic Symbolic Analysis Framework},
  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},
  year = {2016},
  pages = {442--459},