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 Concurrent | A Verification Tool for multi-threaded Java programs |
| Visual DbC | A visualization tool with proof management for programs in the design by contract approach based on KeY. |
| KeY for C | A Verification Tool for the C programming language |
Variants
KeY - A Verification Tool for Java / JavaCard Programs
The current stable release is KeY 1.6.0.
ONE-CLICK LAUNCH: Run KeY 1.6.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://i12www.ira.uka.de/~projekt/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 standard 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 on 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[?]
KeY Concurrent - An Interactive Verification Tool for a Fragment of Multi-threaded Java
The KeY tool has been adapted to a fragment of multi-threaded Java. For more information about this project, please contact Vladimir Klebanov.Visual DbC
Visual DbC is provided as an extension to the Eclipse platform.
Visual DbC provides a graphical notation, called DbC-Notation, that allows to visualize code structure together with specifications in the design by contract approach independent from used languages. Also proofs and references that occur during proof execution, for instance when a method is called, are included. The available tool support allows to create diagrams in that notation from scratch, to generate them from existing source code and to instantiate proofs in a verification tool. As verification tool is KeY, that allows to verify Java code with JML specifications, supported. Other verifications tools are integrable. Notation and tool support together are a powerful proof management tool to support the verification process.
Important Notice
Visual DbC is currently in alpha stage.Download
The extension can be installed using the Eclipse install wizards. Just add the following remote site:
http://www.key-project.org/download/visual-dbc/releases
A user manual is included in the Eclipse help and some example wizards are also provided.
Additional Requirements: In order to install and use Visual DbC the following additional software must be already installed on your computer:
Screenshot: Screenshot of Visual DbC
