Download-2.10 – The KeY Project

Contents

KeY 2.10

KeY 2.10 is the latest stable release and has been published on December 23th, 2021. It comes with many new features under the hood, such as a new SMT translation and completely rewritten parsers for JML and the internal problem and proof format.

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

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.10.0-exe.jar (officially supported install version)
- Download and start via java -jar key-2.10.0-exe.jar
  or via a simple double click on the jar file
Binary Version: key-2.10.0.zip
Source Code: key-2.10.0-sources.tgz
JavaDoc: key-api-doc-2.10.0.zip

Supported Java and JML Features

Changes in KeY 2.10

New ANTLR4 parser for JML
New ANTLR4 parser for the internal problem and proof format
Rewritten translation of problems to SMT-LIB2 and better communication with SMT solvers (currently supported: CVC4 and Z3)
Handling of JML assert/assume-statements via block contracts
Tons of bugfixes, for example:
- fix of a longstanding bug where JML set statements must not be the last statement in a block
- fix for a completeness gap with array types
- fixes for various path handling bugs, in particular when working under Windows
- …
Full changelog

Previous KeY versions

We still provide some previous versions: The previous stable release is KeY 2.8.0. 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.

KeY-Based Eclipse Projects

The Eclipse based projects are not yet updated to KeY 2.10.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 (previous 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.