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:
| KeY | A Verification Tool for Java / JavaCard |
| KeY VBT | A verification-based Test Case Generator |
| 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 |
| KeY for C | A Verification Tool for the C programming language |
| KeY Concurrent | A Verification Tool for multi-threaded Java programs |
Variants
KeY - A Verification Tool for Java / JavaCard programs
Current stable release is KeY 1.4.0.
ONE-CLICK LAUNCH: Run KeY 1.4.0 via Web Start[?]
KeY - Test Case Generator
In addition to formal proofs, the KeY tool allows to generate unit tests from specifications. Start the KeY Test Case Generation version 1.2 or the experimental version 1.5 via Java Web Start[?].
Please note that you additionally need Simplify in a directory
specified by the environment variable PATH as well as
additional libraries such as JUnit in order to compile and run your tests.
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. Just add the following remote site:
http://www.key-project.org/download/releases/eclipse/
Manual for the symbolic debugger (Excerpt of Marcus Baum's diploma thesis - with approval of the author)
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 Web Start[?]: Start KeY-Hoare
- Get the pre-compiled bytecode version: KeY-Hoare-0.1.9.zip
- Source Code version:
KeY-Hoare-0.1.9-src.tgz (README)
- Source-Download required external libraries
- Selected examples (more available on request): KeY-Hoare example problems
Known Issues
KeYmaera - A Deductive Verification Tool for Hybrid Systems
It is a theorem prover extension implementing the calculus for the differential dynamic logic dL. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies.KeYmaera extends the KeY tool with real arithmetic, continuous dynamics 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 and of Andr� Platzer at Carnegie Mellon University.
Download
- KeYmaera: Download, information, examples and tutorials ..
- Run KeYmaera with Web Start[?]