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.