The KeY Project

Integrated Deductive Software Design

The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface.

The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of Karlsruhe Institute of Technology and Chalmers University of Technology, Gothenburg and TU Darmstadt.

The KeY tool is available for download.

If you want to mention KeY in your paper, we recommend that you use the following macro: \newcommand{\KeY}{Ke\kern-0.1emY}


Older News / Events