The KeY Project
Integrated Deductive Software Design
This 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 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 KeY tool is in alpha stage now. Download it from this website.
News
-
KeY-Tutorial: Integrating Object-Oriented Design and Deductive Verification of Software at CADE-20, Tallinn, Estonia, 22-27 July, 2005 (Details)
-
KeY version 0.99 with Java Modeling Language (JML) front-end available.
-
4th International KeY Symposium, June 8th - 10th 2005, Lökeberg Konferenshotell (near Göteborg), Sweden
3rd IEEE International Conference on Software Engineering and Formal Methods, 7-9 September, 2005, Koblenz, Germany
International Conference TABLEAUX 2005, Automated Reasoning with Analytic Tableaux and Related Methods, 14-17 September, 2005, Koblenz, Germany