1 Feature: modular architecture. Created by CMU and NASA since 2010. 2 Two main components: the Executor and the Explorer. Executor is an extension to Java PathFinder. 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.

6

11 They said, JCute and JFuzz 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 Java PathFinder for dealing with native code. In the table with result their tool marked as tool with native code support (as well as Symbolic PathFinder and JFuzz).

Sergey Vartanov, 2007–2020