Traditionally, KeY was a program verification tool for Java. Although this still is one of its main applications,
it grew over the years to a program verification platform with various fields of application.
The currently most prominent applications are:
- Program Verification (Standalone GUI, Eclipse Integration, KeYHoare)
- Debugging (Symbolic Execution Debugger)
- Information Flow Analysis / Security
- Test Case generation (KeYTestGen)
We are constantly working on making the KeY framework more accessible for other applications. For instance,
it is quite easy to use KeY as a symbolic execution engine in the backend of another tool.
Ongoing work includes, for instance, the construction of a Java compiler based on symbolic execution trees
created by KeY.