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}
News
-
KeY 2.0.0 has been released. Download it now!
-
KeY 1.6.5 has been released as maintenance release, providing Java 7 compatibility.
The 11th International KeY Symposium takes place July 22-25, 2012
The book on KeYmaera Logic Analysis of Hybrid Systems by André Platzer covering logic and tool KeYmaera (based on KeY) is now available.