Overview

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:

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.