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
-
7th International KeY Symposium 08, 4th-6th June in Gothenburg, Sweden
-
KeY is now part of COST Action IC0701, a European research network on "Formal Verification of Object-Oriented Software".
-
KeY 1.2.0 has been released. Download it now!
- 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
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