-
Notifications
You must be signed in to change notification settings - Fork 0
KeY is a deductive program verifier for Java programs. The core features of KeY are:
- Support of a large subset of the Java language, including loops, recursion, exceptions, integer types with overflows, floating point types, inheritance, static initialization, ...
- Modular specification/verification
- Reasoning via Dynamic Logic for Java (JavaDL) and sequent calculus
- Memory/heap modeling via Dynamic Frames
- Program transformation to first-order via Symbolic Execution
- Automatic strategy for proof search with possibility to also manually inspect the proof situation and apply rules/macros
Java programs, specifications in the Java Modeling Language (JML).
KeY supports Java programs. For remarks on the supported Java features see https://www.key-project.org/applications/program-verification/.
KeY is able to verify functional correctness according to a given specification in the Java Modeling Language (JML). This also includes proofs of termination. In addition, KeY can be used to verify relational properties between multiple programs or program runs, for example (absence of) information flow.
The reasoning in KeY works via a Dynamic Logic for Java (JavaDL) and built-in sequent calculus rules. Proof search is carried out by the built-in strategies and macros or via user interaction. Symbolic Execution is used to transform programs and specifications to first-order proof obligations.
Optionally, KeY can make use of SMT solvers via a translation of the problem to SMT-LIB:
- Z3
- CVC4
- cvc5
- PRINCESS
In case the specification is not valid, Z3 can also be used to obtain counterexamples.
- https://www.key-project.org/ (for documentation and information)
- https://github.com/KeYProject/key (for the released binaries, development, issue reporting, and discussions)
KeY is written in Java, the jar file can be directly downloaded and executed (assuming Java 11 or newer is installed).
Example files are shipped with the tool, see here: https://github.com/KeYProject/key/tree/main/key.ui/examples
The main reference is the second KeY book, which explains the underlying concepts and most features of KeY in detail:
[1] Ahrendt, Wolfgang, Beckert, Bernhard, Bubel, Richard, Hähnle, Reiner, Schmitt, Peter H., Ulbrich, Mattias (Ed.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer, 2016, ISBN: 978-3-319-49811-9.
Preprints of the chapters are also available: https://www.key-project.org/thebook2/
The extensive list of all KeY-related publications can be found here: https://www.key-project.org/publications/