This repository is the home of the interactive theorem prover KeY for formal verification and analysis of Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a library e.g. for symbolic program execution, first order reasoning, or test case generation.
For more information, refer to
- The KeY homepage
- The KeY book
- The KeY developer documentation
- KeY's success stories:
The current version of KeY is 2.12.2, licensed under GPL v2.
Feel free to use the project templates to get started using KeY:
- Hardware: >=2 GB RAM
- Operating System: Linux/Unix, MacOSX, Windows
- Java 17 or newer
- Optionally, KeY can make use of the following binaries:
This folder provides a gradle-managed project following
Maven's standard folder layout.
There are several subprojects in this folder. In general, every key.*/ subproject contains a core component of KeY.
Additional and optional components are in keyext.*/ folders. The file build.gradle is the root build script
describing the dependencies and common build tasks for all subprojects.
key.util, key.core and key.ui are the base for the product "KeY Prover". Special care is needed
if you plan to make changes here.
Assuming you are in the directory of this README file, you can create a runnable and deployable version with one of these commands:
-
With
./gradlew key.ui:runyou can run the user interface of KeY directly from the repository. Use./gradlew key.ui:run --args='--experimental'to enable experimental features. -
Use
./gradlew classesto compile KeY, which includes running JavaCC and Antlr. Likewise, use./gradlew testClassesif you also want to compile the JUnit test classes. -
Test your installation with
./gradlew test. Be aware that this will usually take multiple hours to complete. With./gradlew testFast, you can run a more lightweight test suite that should complete in a few minutes.You can select a specific test case with the
--testsargument. Wildcards are allowed../gradlew :key.<subproject>:test --tests "<class>.<method>"
You can debug KeY by adding the
--debug-jvmoption, then attaching a debugger atlocalhost:5005. -
You can create a single jar-version, aka fat jar, of KeY with
./gradlew :key.ui:shadowJar
The file is generated in
key.ui/build/libs/key-*-exe.jar. -
A distribution is build with
./gradlew :key.ui:installDist :key.ui:distZip
The distribution can be tested by calling
key.ui/install/key/bin/key.uiand is zipped inkey.ui/build/distributions.The distribution gives you potential of using single jar files.
-
Quality is automatically assessed using SonarQube on each pull request. The results of the assessments (pass/fail) can be inspected in the checks section of the PR.
The rules and quality gate are maintained by Alexander Weigl [email protected] currently.
-
More guideline and documentation for the KeY development can be found under key-docs.
-
For bug reports, please use the issue tracker or send a mail to [email protected].
-
For discussions, you may want to subscribe and use the mailing list [email protected] or use GitHub discussions.
Feel free to submit pull requests via GitHub. Pull requests are assessed using automatic tests, formatting and static source checkers, as well as a manual review by one of the developers. More guidelines and documentation for the KeY development can be found under key-docs.
This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
Universität Koblenz-Landau, Germany
and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
Technical University Darmstadt, Germany
Chalmers University of Technology, Sweden
The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.