PV3 JDartchecks properties of annotated Java code with dynamic symbolic execution

JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A constraint solver is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths.

Application domain/field

Expected input


Expected output

Reports assertion violations


JDart is built on top of the JPF software model checker and uses the JConstraints library for the integration of constraint solvers.


License: Apache-2.0


Related papers

Last publication date

17 April 2020

Related tools

Other tools that participated in the JavaOverall category of SV-COMP in 2020: Java-Ranger, JBMC, COASTAL, JayHornSPF

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.