PV3 ⊧ JDartchecks properties of annotated Java code with dynamic symbolic executionJDart 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.
- Dynamic symbolic execution
- Java programs
- Constraint solver
- Concolic execution
- Program annotated with assertions
- Analysis configuration
- Analysis configuration: jpf application properties file (