New Readme

KeY -- Deductive Java Program Verifier

This repository is the home of the interactive theorem prover KeY, which allows you to apply formal verification techniques on Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional of Java using the Java Modeling Language. But KeY can also be used as a library.

For more information refer to the

• Homepage
• The second KeY book
• Developer Documentation

You can find the releases on Github or on Maven Central

Feel free to use the project templates to get starting using KeY:

• For Verification Projects
• Using as a Library
• Using as a Symbolic Execution

Help Requests, Issues and Bug Reports

If you encounter problems, feel free to them in.

• For bug reports you should use the issue tracker. If you may want to send confidential information or file in a vulnerability, you should use support@key-project.org.

• For discussions, you may want to subscribe and use the mailing list key-all@lists.informatik.kit.edu or just use Github discussions

Requirements

• Hardware: >=2 GB RAM
• Operating System: Linux/Unix, MacOSX, Windows
• Java 17+ since KeY 2.12.0
  • Version 11 for KeY 2.12.0 or older release
• Optionally, KeY can make use of the following binaries:
  • SMT Solvers: Z3, CVC5, CVC4 Princess

Building

KeY is build with gradle and therefore follows the Maven's standard folder layout. KeY consists of multiple modules. Modules starting with key. contains a core component of KeY, in contrast optional extensions start with keyext.. The modules 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.

Obtain a runnable version of KeY

1. With ./gradlew key.ui:run you can run the user interface of KeY directly from the repository. Use ./gradlew key.ui:run --args='--experimental' to enable experimental features.

2. Use ./gradlew classes to compile KeY, which includes running JavaCC and Antlr. Likewise, use ./gradlew testClasses if you also want to compile the JUnit test classes.

3. 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 --tests argument. Wildcards are allowed.

   ./gradlew :key.<subproject>:test --tests "<class>.<method>"

   You can debug KeY by adding the --debug-jvm option, then attaching a debugger at localhost:5005.

4. 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.

5. 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.ui and is zipped in key.ui/build/distributions.

   The distribution gives you potential of using single jar files.

Developing KeY

• 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 weigl@kit.edu currently.

• More guideline and documentation for the KeY development can be found under key-docs.