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 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
-
Andre Platzer and Edmund M. Clarke receive the Best Paper Award of FM 2009 for their work on verification of Curved Flight Collision Avoidance Maneuvers with KeYmaera which is based on the KeY system.
-
8th International KeY Symposium 09, 18th-20th May in Speyer, Germany
-
KeY 1.4.0 has been released. Download it now!
-
KeY is now part of COST Action IC0701, a European research network on "Formal Verification of Object-Oriented Software".
KeYmaera: 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.
- 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