Download-2.8 – The KeY Project

Contents

KeY 2

KeY 2.8 is the latest stable release and has been published on December 18th, 2020. It comes with an overhauled user interface and many new features.

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

Previous KeY versions

We provide still some previous versions:
The versions KeY 2.6.x accompany the second KeY Book. You can find the KeY 2.6.x versions here. 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.

Download or Start

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

Single Click Jar: KeY-2.8.0.jar (officially supported install version)
- Download and start via java -jar key-2.8.0-exe.jar
  or via a simple double click on the jar file
Binary Version: KeY-2.8.0.zip
Source Code: KeY-2.8.0-src.zip

Supported Java and JML Features

New Features in 2.8

Support for bounded sums
Innovative and improved treatment of loops via loop contracts and a new loop invariant rule based on loop scopes
Proof bundles: Saving proofs incl. resources into one zip file
Source code view with highlight for symbolically executed statements
Origin Labels: Track the origin of the formulas (e.g. if they stem from a precondition, postcondition or loop invariant)
Heatmaps (know which formulas have been modified recently)
Interaction Logging
Flexible and configurable layout, Improved search, proof exploration, etc.
New proof script command
Full changelog

KeY-Based Eclipse Projects

The Eclipse based projects are not yet updated to KeY 2.8.0. The linked versions are still based on KeY 2.6.3.

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

Update Site Name:	KeY Eclipse Extensions
Update Site URL:	https://formal.iti.kit.edu/key/download/releases/2.6/eclipse/

Unstable Development Versions (Nightly Builds)

You can download a current snapshot of the KeY development version below.

	Just download and start via `java -jar key*-exe.jar`.
Source and Binary Artefacts	The classical KeY distribution containing a single jar file with all components, sources and JavaDoc files.

Maven Repository

If you intend to use KeY as a (Java) library and want to access its API, you can include KeY as a dependency in Maven, gradle, sbt (or similar managers). We provide a Maven repository that contains the artifcats for the KeY packages mentioned below. The repository contains the current official release and is irregularly updated with the stable nightly-build version.

The Maven repository is hosted at our Gitlab instance. For using KeY you should include key.core or key.ui into your build script.

URL	https://git.key-project.org/api/v4/projects/35/packages/maven
Group Id	org.key_project
Artifacts Id	key.core key.ui
Version:	2.8.0 (current release) 2.6.3 (old release) 2.9.0-SNAPSHOT (weekly-published nightly build)

Other artifacts are also exported, and are included transitively if required.

Example Project

You can find an example project on how to use KeY with Gradle here: https://github.com/KeYProject/key-java-example

Use with Maven

<repositories>
  <repository>
    <id>gitlab-maven</id>
    <url>https://git.key-project.org/api/v4/projects/35/packages/maven</url>
  </repository>
</repositories>

Use with Gradle

repositories { 
  maven { 
    url  "https://git.key-project.org/api/v4/projects/35/packages/maven"    
  }
}

Using the Public Repository

Beside of the zipped distribution you have access to a mirror of the internal Git repository. The mirror contains the stable (tested and validated master) and release branches of KeY. You can find the repository here:

https://git.key-project.org/key-public/key/

Using the public repository is the best choice, if you use (a) gradle for building your project and (b) you plan to make changes to KeY. Then you should add KeY as a submodule to your project:

$ git submodule add https://git.key-project.org/key-public/key.git

And add to your settings.gradle:

includeBuild 'key/key'

Known Problems & Workarounds

Strings “don’t work” in projects with auto-generated stubs

Problem description	Reason	Workaround
When using the (otherwise very practical!) feature of the KeY eclipse plugin which automatically generates stubs (empty methods with default specifications) for included library methods, it might happen that symbolic execution of Java programs gets stuck at a place like `str = "foo";`, where `str` is a variable of type String.	Normally, String assignments just work, since this behavior is defined in some files shipped with KeY (JavaRedux). However, when generating stubs (that are included via the “bootclasspath” option), the default behavior is overidden by the dummy behavior, resulting in certain elementary things not working.	The workaround is to replace the content of the file “String.java” in the folder “stubs/java/lang/” with the content of the “String.java” originally shipped with KeY, and to furthermore add a file “String.key“ in the same directory (click on the links to download current versions of those files as of 2018/01/25). Now, String assignments should work again.