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

• Dynamic symbolic execution
• Java programs
• Constraint solver
• Concolic execution

Expected input

• Program annotated with assertions
• Analysis configuration

Format:

• Program: .java
• Analysis configuration: jpf application properties file (.jpf file)

Expected output

Reports assertion violations

Internals

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

Comments

License: Apache-2.0