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.
Call for participation in the Understanding Proof Attempts Evaluation
The 14th International KeY Symposium takes place 27th July - 29th July, 2015
KeY 2.4.1 has been released on February 19, 2015. Download it now!