KeY 2
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 Start
KeY requires Java 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
KeY-Based Eclipse Projects
Add the best matching update-site to your Eclipse release to install the listed KeY-based projects:
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
| Project | Explanation | Category | Status |
|---|---|---|---|
| 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 |
JML Editing and Stubby are available on the preview update site.
For an optimal user experience it is recommended to use at least the following JVM memory settings:
- -Xms128m
- -Xmx1024m
- -XX:MaxPermSize=256m
They can be changed in the "eclipse.ini" file or by starting Eclipse with the following additional parameters:
-vmargs -Xms128m -Xmx1024m -XX:MaxPermSize=256m
Addons
KeY 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.
Documentation
- Quicktour for KeY 2.x
- More documentation and material will be available soon!
License
KeY is distributed under the GNU General Public License.Support
Send an email to support@key-project.orgFeature Preview of KeY-Based Eclipse Projects
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.
Update Site URL: http://www.key-project.org/download/releases/eclipse-preview/luna
| Project | Explanation | Category | Status |
|---|---|---|---|
| JML Editing | JDT extension to support JML. | Editing | Beta |
| Stubby | Stub Generation of used API members. | Utilities | Beta |
Unstable development builds (nightly builds)
No support is provided for development versions.- Download development versions.