KeY Project: Integrated Deductive Software Design

KeY 1.6.0

KeY 1.6.0 is the current stable release. It has been released on October 6, 2010.

KeY is distributed under the GNU General Public License.

Java version 6 or newer
Supported platforms: Linux, Solaris, Mac OS X, Windows 2000 or above (Windows in bytecode distribution or Java Web Start only)

ONE-CLICK LAUNCH
Run KeY 1.6.0
via Web Start^[?]

For getting KeY 1.6.0, choose one of the following options:

Start it directly via Web Start^[?] using the "Run KeY 1.6.0" link on the right
Download the pre-compiled bytecode version: KeY-1.6.0.tgz or KeY-1.6.0.zip, README-1.6.0.txt, required libraries
Compile it from source: KeY-1.6.0-src.tgz, README-1.6.0-src.txt, required libraries

Additionally, you may want to use:

External SMT solvers
The following Eclipse plug-in update site, which offers a rudimentary Eclipse integration of KeY:
```
http://i12www.ira.uka.de/~projekt/download/releases/eclipse
```

Other versions (no support provided):

Nightly builds allow access to the latest development versions (Run current version via Web Start^[?])
Older releases

A collection of examples (already included in bytecode and sourcecode distribution): examples-1.6.zip
The best source for information on KeY is the KeY Book. In particular, chapter 10 provides a thorough introduction to the system. We provide also updated examples of the KeY Book for KeY-1.6.0 (BookExamples-1.6.zip)
There are several case studies and tutorials that introduce to the main functions of KeY and show how KeY handles more extensive contexts. In particular, we recommend the KeY Quicktour as an introduction.
A cheat sheet for the KeY-Syntax (draft).