The Dart, the Psyco, and the Doop: Concolic Execution in Java PathFinder and its Applications


Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Zvonimir Rakamaric, Vishwanath Raman. Java Pathfinder Workshop (JPF 2014), Salt Lake City, UT, USA.
[pdf] [bib]

Abstract: JDart is a concolic execution extension for Java PathFinder. Concolic execution executes programs with concrete values while recording symbolic constraints. In this way, it combines the benefits of fast concrete execution, with the possibility of generating new concrete values, triggered by symbolic constraints, in order to exercise additional, potentially rare, program behaviors. As is typical with concolic execution engines, JDart can be used for test-case generation. Beyond this basic mode, it has also been used as a component of other tools. In this paper, we describe the main features of JDart, provide usage examples, and give an overview of applications that use JDart. We particularly concentrate on our efforts into making JDart robust enough to handle large, complex systems.


  author = {Marko Dimja\v{s}evi\'c and Dimitra Giannakopoulou and Falk Howar and Malte Isberner
    and Zvonimir Rakamari\'c and Vishwanath Raman},
  title = {The {Dart}, the {Psyco}, and the {Doop}: Concolic Execution in {Java} {PathFinder}
    and its Applications},
  journal = {ACM SIGSOFT Software Engineering Notes},
  volume = {40},
  number = {1},
  year = {2015},
  month = {January},
  pages = {1--5},
  publisher = {ACM},
  note = {Proceedings of the 2014 Java Pathfinder Workshop (JPF)},