KeYTestGen is a white-box test generator for Java methods based on
KeY's program analysis and symbolic execution. KeYTestGen generates a JUnit
test harness (test driver) which does not only initialize method parameters
but also the global state that is defined by the (potentially private)
fields of objects and classes. For example, a complex linked data structure
may be created as test input. The tests can satisfy different test criteria
such as branch coverage, path coverage, and MC/DC coverage. The user may
also provide a specification in the Java Modeling Language (JML) from which
a test oracle can be generated or which can be used as an abstraction for a
loop or method call. KeYTestGen can be used either as a simple stand-alone
tool not requiring expert knowledge or it can be used in an advanced way to
support and complement formal verification.