The KeY Project
Integrated Deductive Software Design
The aim of the project is to integrate formal software specification and verification into the industrial software engineering processes. The starting point is a commercial CASE tool, which is augmented by capabilities for formal specification and verification. The ultimate goal is to make the verification process transparent for the user with respect to the informal object-oriented model. Get the KeY tool product sheet.
The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of the University of Karlsruhe, Chalmers University of Technology, Gothenburg, and the University of Koblenz. The project is funded by DFG and Vinnova. There is also a number of project affiliates.
The KeY tool is available for download.
News
- Now supporting Java Webstart: Run KeY with just two mouse clicks in one minute - works on any computer with at least Java 1.4.1
HyKeY: A theorem prover for differential dynamic logics (based on KeY) has been released by the AVACS group of Prof. Dr. E.-R. Olderog, University of Oldenburg.
-
KeY 1.0 has been released. Download it now!
-
6th International KeY Symposium, June 14th - 16th 2007, Eisenbachtal, Germany
- The book on KeY is now available -
the definite source for all information related to the KeY project
Verification of Object-Oriented Software:
The KeY Approach
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.)
15 chapters and 2 appendices, xxix + 658 pages
ISBN: 3-540-68977-X
Springer-Verlag, LNCS 4334 - BibTeX - Book Website