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.
News
-
The 15th International KeY Symposium takes place 25th July - 28th July, 2016
-
Tutorial about The Sequent Calculus of the KeY Tool presented at CADE-25
-
The 14th International KeY Symposium takes place 27th July - 29th July, 2015
Proving that Android's, Java's and Python's sorting algorithm is broken (and showing how to fix it)
-
KeY 2.4.1 has been released on February 19, 2015. Download it now!