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.
KeY 2.2.2 has been released. Download it now!
The 13th International KeY Symposium takes place 29th September - 1st October, 2014
KeY 2.2.1 has been released. Download it now!
The 12th International KeY Symposium takes place 30th September - 2nd October, 2013
KeY 2.0.1 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