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 |
| - Visual DbC | A visualization tool with proof management for programs in the design by contract approach based on KeY 1.6 (official release). |
| - MonKeY | Batch verification of all proof obligations based on KeY 2.0 technology preview (ca3789c2b79d7c603f5e354999ce275469aaa029). |
| 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 |
| 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[?]
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 1.6, 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
MonKeY
MonKeY is provided as Eclipse product.
MonKeY provides a simple user interface that allows to prove a whole project automatically in KeY. The tool creates all proof obligations for the specified program and tries to prove them with KeY in automatic mode. Finally the user can export the verification result as CSV file.
Important Notice
MonKeY is currently in alpha stage.Download
The tool is available as Eclipse product. Use one of the following download links:
Linux based on KeY 2.0 technology preview (ca3789c2b79d7c603f5e354999ce275469aaa029)
Mac OS X based on KeY 2.0 technology preview (ca3789c2b79d7c603f5e354999ce275469aaa029)
Instructions:
- Extract the downloaded archive and start the product.
-
Enter the source code location or the file to load in field "Location".
Optionally, define a boot class path location or keep it empty. - Click on "Load". Wait until the table is filled with proof obligations.
- Optionally, change some of the proof search strategy options
- Click on "Start all proofs". Wait until KeY has tried to close all obligations automatically.
- Optionally, close still open proofs in the user interface of KeY manually
- Optionally, export the result as CSV file by clicking on "Export".
MonKeY provides also a batch mode which can be used to verify different source locations multiple times. To use the batch mode start MonKeY (MonKeYC in windows) with parameters "-batch -noSplash" and read the printed documentation for further information.
Screenshot: Screenshot of MonKeY
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[?]