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 10th International KeY Symposium takes place August 26-27, 2011, conjunction with the 2nd International conference on Interactive Theorem Proving, ITP 2011, Nijmegen, The Netherlands
The book on KeYmaera Logic Analysis of Hybrid Systems by André Platzer covering logic and tool KeYmaera (based on KeY) is now available.
-
KeY 1.6.0 has been released. Download it now!
KeY successful at the VSTTE'10 verification competition.
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