KeY 2.4.1 is the latest stable release, released on February 19, 2015.
KeY 2 differs significantly from the previous KeY 1.6 release. The older KeY 1.6 release is currently still maintained and available as KeY 1.6.5 (released on April 18, 2013).
KeYmaera and other KeY variants like KeY-Hoare can be found here.
Download or StartJava version 6 or newer and is tested on Linux, OS X and Microsoft Windows.
- Instant Start: Web Start[?]
- Binary Version: KeY-2.4.1.tgz or KeY-2.4.1.zip, README-2.4.1.txt, required libraries
- Source Code: KeY-2.4.1-src.tgz, README-2.4.1-src.txt, required libraries
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
Update Site URL: http://www.key-project.org/download/releases/eclipse/luna
Update Site URL: http://www.key-project.org/download/releases/eclipse/kepler
Update Site URL: http://www.key-project.org/download/releases/eclipse/juno
Update Site URL: http://www.key-project.org/download/releases/eclipse/indigo
|KeY 4 Eclipse Starter||A basic Eclipse extension to start KeY from within Eclipse.||Verification||Release|
|KeYIDE||An alternative user interface for KeY directly integrated into Eclipse.||Verification||Beta|
|KeY Resources||Provides the "KeY project" with automatic background proofs.||Verification||Release|
|MonKeY||Batch verification of all proof obligations.||Verification||Release|
|Symbolic Execution Debugger (SED)||A debugger based on symbolic execution.||Debugging||Release|
|Visual DbC||A proof management and visualization tool.||Visualization||Release|
For an optimal user experience it is recommended to use at least the following JVM memory settings:
They can be changed in the "eclipse.ini" file or by starting Eclipse with the following additional parameters:
-vmargs -Xms128m -Xmx1024m -XX:MaxPermSize=256m
AddonsKeY can optionally use SMT solvers to improve automation:
In addition to directly supporting these solvers, KeY provides an export into the SMT-LIB file format. Bindings for new SMT solvers supporting this format can be added easily, in case of interest please ask the KeY group for assistance.
- Quicktour for KeY 2.x
- More documentation and material will be available soon!
LicenseKeY is distributed under the GNU General Public License.
SupportSend an email to firstname.lastname@example.org
The following update-site is based on newer KeY versions and offers a preview of future features. Due to the non final status, productive use is not recommended.
|JML Editing||JDT extension to support JML.||Editing||Beta|
|Stubby||Stub Generation of used API members.||Utilities||Beta|
- Download development versions.