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
• Success Stories: Bug found in TimSort, Verification of java.util.IdentityHashMap, Google Award for bug in LinkedList

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 [email protected].

• For discussions, you may want to subscribe and use the mailing list [email protected] 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

You can create the 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.

Further tasks of generated are

• ./gradlew key.ui:run to start the the user interface directly. You can submit program arguments with --args, e.g., ./gradlew key.ui:run --args='--experimental'.

• Execute all tests with ./gradlew test or ./gradlew testFast. Be aware that this will usually take multiple hours to complete.

Contributing KeY

Feel free to submit Pull Requests via Github. Pull Requests are assessed using an automatically tests, formatting and static source checkers. More guideline and documentation for the KeY development can be found under key-docs.