Download

KeY 2

KeY 2.6.2 is the latest stable release, released on April 18th, 2017.
The versions KeY 2.6.x accompany the second KeY Book.

For major new features (like state merging etc.), please checkout the nightly build.

KeY 2 differs significantly from the previous KeY 1.6 release.
The last KeY 1.6 release is KeY 1.6.5 (released on April 18, 2013) and only provided for legacy reasons.

KeY Hoare has its own dedicated download page.

In case of questions about KeY please contact: support@key-project.org.

Download or Start

KeY requires Java version 7 or newer and is tested on Linux, OS X and Microsoft Windows.

Supported Java and JML Features

New Features in 2.x

  • Explicit Heap Model and Dynamic Frames
  • Verification of Recursive Methods
  • Further Enhancend JML Support (Details)
  • Simplified representation of integers
  • GUI improvements (refreshed appearance, improved search, keyboard shortcuts)
  • Counter Example Generation & Test Generation
  • Calculus for Information Flow Reasoning
  • Full support for shift-operations and partially for other binary operators
  • Various bugfixes

KeY-Based Eclipse Projects

Detailed information about the provided Eclipse extensions can be found here.
To install KeY 2.6.1 for Eclipse 4.6 Neon (other 4.x versions (Luna/Mars) should work as well)

Update Site Name: KeY Eclipse Extensions
Update Site URL: http://i12www.ira.uka.de/key/download/releases/2.6/eclipse/

Known issues

If no items are shown in the “Install” wizard, please deselect the checkbox “Group items by category”.

Unstable Development Versions (Nightly Builds)

Download development versions.

Attention: The nightly builds require Java 8 and a JRE/JDK with JavaFX. JavaFX is included in the Oracle JDK. In case of OpenJDK it depends on your distribution (for Ubuntu: please install openjfx via sudo apt-get install openjfx)

No support is provided for development versions.

Run Nightly Build via Webstart

Have a look at the section Webstart Problems
if you have trouble starting KeY via Webstart

Webstart Problems

These issues are most likely only of concern if you are using webstart for the nighlty builds.

If you get an error dialog stating that the execution of the application was blocked due to your Java security settings, you have three options.
You can either

  • download and run the binary versions using the links provided above,
  • add the website http://i12www.ira.uka.de/ to the exception list of your Java installation, or
  • import our certificate with which the Jar was signed.

Adding our website to the exception list

First, you have to start the Java Control Panel. This can be accomplished via running javaws -viewer in a terminal. Two windows should open: The “Java Cache Viewer” (close this window) and the Java Control Panel. Click on the “Security” tab in the control panel and choose to edit the site list; then, click on “Add” and enter the URL http://i12www.ira.uka.de/.

Import the KeY certificate

Download the file “KEY.cer” which contains our certificate. Open the Java Control Panel via running javaws -viewer and close the cache viewer. Click on the “Security” tab and choose to manage certificates. Then, click on “import”, change the file filter to “All Files”, navigate to the directory where you stored the KEY.cer file, choose it and press OK.

If the two solutions outlined above should fail for you, please resort to downloading and using the compiled binary version.