KeY 2.6.x (Book Version) – Download

Contents

KeY 2.6.x

The versions KeY 2.6.x accompany the second KeY Book. For major new features (like state merging etc.), please check out 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.

Run KeY 2.6 via Webstart

Download or Start

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

Instant Start: Web Start
Binary Version: KeY-2.6.3.zip
Source Code: KeY-2.6.3-src.tgz

Supported Java and JML Features

New Features in 2.x

Explicit Heap Model and Dynamic Frames
Verification of Recursive Methods
Further Enhanced 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 bug fixes

KeY-Based Eclipse Projects

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.kastel.kit.edu/~key/download/releases/2.6/eclipse/

Maven Repository

We provide a Maven repository via Bintray. The repository is irregularly updated with our current stable version.

URL	https://dl.bintray.com/key/stable-snapshots/
Group Id	org.key_project
Artifacts Id	key.core.example key.core.proof_references key.core.symbolic_execution.example key.core.symbolic_execution key.core.testgen key.core key.removegenerics key.ui key.util keyext.interactionlog rifl
Version:	2.7.0.YYYYMMDD

You also need recoder:

key-project:recoderKey:1.0

Use with Maven

<repository>
   <snapshots><enabled>false</enabled></snapshots>
   <id>bintray-key-stable-snapshots</id>
   <name>bintray</name>
   <url>https://dl.bintray.com/key/stable-snapshots</url>
</repository>

Use with Gradle

repositories {     
  maven {        
    url  "https://dl.bintray.com/key/stable-snapshots"    
  } 
}

Webstart Problems

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 https://formal.kastel.kit.edu/ 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 https://formal.kastel.kit.edu/.

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.

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