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 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

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.

7th International KeY Symposium 08, 4th-6th June in Gothenburg, Sweden

KeY-Tutorial: Integrating Verification and Testing of Object-Oriented Software at TAP 2008, Prato, Italy, April 9th, 2008

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

KeY 1.0 has been released. Download it now!

KeY-Tutorial: Integrating Object-Oriented Design and Deductive Verification of Software at IFM 2007, Oxford, UK, 3rd July 2007

6th International KeY Symposium, June 14th - 16th 2007, Eisenbachtal, Germany

KeY-Tutorial: Integrating Object-Oriented Design and Deductive Verification of Software at SEFM 2006, Pune, India, 11-15 September 2006

5th International KeY Symposium, June 6th - 8th 2006, Speyer, Germany

KeY version 1.0-pre1 (incl. UML/OCL, JML and DL front-end) available.

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

3rd International KeY Symposium, 7 - 9 June, 2004, Königswinter/Koblenz, Germany

• Workshop OCL 2.0 - Industry Standard or scientific playground? at UML 2003,
  21 October, 2003, San Francisco

• Tutorial on "Integrating Object-oriented Design and Deductive Verification of Software" at FME 2003,
  9 September, 2003, Pisa, Italy

• 2nd Swedish-German KeY Workshop, 10 - 12 June, 2003, Bad Herrenalb, Germany