: A Dynamic Symbolic Analysis Framework
1 Feature: modular architecture. Created by and since 2010. 2 Two main components: the Executor and the Explorer. Executor is an extension to . Explorer determines the exploration strategy. It uses JConstraints library (also their work). 3 Thay said, path constraints are combined into constraints tree. 5 It executes Java bytecode. It also generates method summaries and jUnit tests. It can analyze the whole program as well as method. As a plugin to JPF, JDart implements:
- setting concrete values (mark points to back track),
- recording symbolic constraints.
11 They said, and are no longer actively maintained.
They could deal with native methods from java.lang.Math. Only with them, or with any native method? They said, there is an extension to for dealing with native code. In the table with result their tool marked as tool with native code support (as well as and ).
Sergey Vartanov, 2007–2020