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
KeY successful at the VSTTE'10 verification competition.
The 9th International KeY Symposium takes place May 25-27, 2010 in Gernsbach near Karlsruhe
Version 1.8 of KeYmaera: A theorem prover for differential dynamic logics (based on KeY) has been released.
-
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.
- 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