Download KeY
While KeY is mainly aimed at verification of Java / JavaCard programs, recent research has produced a number of KeY variants to handle related problems.
The following variants of the KeY tool are available here for download:
| KeY | A Verification Tool for Java / JavaCard and a Test Case Generator |
| KeY for C | A Verification Tool for the C programming language |
| Symbolic Execution Debugger | A debugger application that completely hides the theorem prover interface of KeY. Realized as an Eclipse plugin. |
| KeY-Hoare | A Verification Tool for the Hoare Calculus |
| KeYmaera (formerly HyKeY) | A Verification Tool for Hybrid Systems |
License
KeY is distributed under the GNU General Public License.
Requirements
- Java JDK 1.4.1 or newer.
Supported platforms: Linux, Solaris, Windows 2000 or above (Windows in bytecode distribution or Java Web Start only). - Recommended add-ons
Documentation
Updated tutorials and examples for KeY 1.2.0 will be made available soon.- The best source for information on KeY is the KeY Book. In particular chapter 10 provides a thorough introduction to the system.
- There are several tutorials that introduces to the main functions of KeY - both for JML and OCL.
- Larger case studies show how KeY handles more extensive contexts.
- Collection of examples (already included in the source distribution).
Support
Send an email to support@key-project.orgKeY - An Interactive Verification Tool for JavaCard programs
Front-ends
The current release version is 1.2.0. It includes the following front-ends:- UML/OCL (requires a Borland Together product; see below)
- JML (Java Modeling Language)
- Standalone KeY-Prover (JavaDL)
Test case generation
In addition to formal proofs, this version allows to generate unit tests from specifications (Start the KeY Test Case Generation standalone version via Java Webstart).Download
KeY Version 1.2.0- Start KeY via Java Webstart - Info to Webstart
- Get the pre-compiled bytecode version: KeY-1.2.0.tgz (README, ChangeLog)
- Compile KeY from source: KeY-1.2.0-src.tgz (README, ChangeLog)
- Download required external libraries
- Available add-ons (Grammatical Framework, Simplify, SMT-LIB support)
- Nightly builds allow access to the latest development versions (also as Webstart - Info)
- Remote site for nightly build eclipse plug-ins: http://i12www.ira.uka.de/~bubel/nightly/eclipse/
- and Older versions
Known Issues
The published version has some known problems and limitations: Known IssuesKeY for C - An Interactive Verification Tool for the C Programming Language
The KeY tool has been adapted to the C programming language also. Soon, you will find the according downloads here.Symbolic Execution Debugger
The Symbolic Execution Debugger is provided as a plugin to the Eclipse development platform.
A new debugging approach is presented by introducing a software debugger which is based on visualizing symbolic program executions. Symbolic execution is a program analysis technique that runs a program with symbolic input values representing unknown values in order to explore all possible program executions. An obvious benefit of such a debugger is that symbolic execution explores all possible program executions, and it thus can be used for finding program executions that are not intended by the programmer. Symbolic execution captures the entire behavior of a program up to a certain point. So once a bug is recognized, the debugger can also be used to find the origin of the bug in the source code, the reason for the misbehavior and sometimes even possible fixes.
Important Notice
The symbolic debugger extension is currently in alpha stage.Download
The plugin can be installed using the Eclipse plugin install. Therefore a remote site referring to
Additional Requirements: In order to install and use the Symbolic Debugger the following additional software must be already installed on your computer:
- the Eclipse IDE and
- the Eclipse plugin Graphical Editing Framework (GEF). GEF is not part of the default Eclipse installation, but can be installed via the Callisto project offered in the Eclipse Software Install.
Screenshots: Symbolic State View · Execution Tree
KeY-Hoare - An Interactive Verification Tool for the Hoare Calculus
The core KeY Tool uses dynamic logic as underlying logic. The Hoare Calculus is another possibility to deal with programs in logic. KeY-Hoare is built on top of KeY and features a Hoare calculus with updates. It is used in the Chalmers undergraduate course Program Verification to teach the Hoare calculus. [ More information ]
Download
- Use Java Webstart: Start KeY-Hoare
- Get the pre-compiled bytecode version: KeY-Hoare-0.1.6.zip
- Source Code version:
KeY-Hoare-0.1.6-src.tgz (README)
- Source-Download required external libraries
Known Issues
KeYmaera - A Deductive Verification Tool for Hybrid Systems
KeYmaera (formally known as HyKeY) is a deductive verification tool for hybrid systems.It is a theorem prover extension implementing the calculus for the differential dynamic logic dL.
KeYmaera extends the KeY tool with Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems.
It has been developed in the group of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg.
Download
- Get the installation script:
KeYmaera
- Requirements: Java 5 and Mathematica
- More information, examples and tutorials ...
1 Excerpt of Marcus Baum's diploma thesis - with approval of the author.