This page gathers various resources around the KeY Verification Tool for Java and the Java Modelling Language (JML).
-
https://github.com/KeYProject/ips4o-verify
New very fast sorting algorithm. TACAS'24
-
https://github.com/KeYProject/VerifyingIdentityHashMap
java.util.IdentityHashMap -- Best paper, iFM'22
-
https://github.com/KeYProject/BitSet-KeY-Artifact
java.util.BitSet, FACS'23
-
https://github.com/KeYProject/rbtree-verification
Red-Black Trees
-
https://github.com/KeYProject/DualPivotQuickSort
Dual Pivot Quicksort: One of the standard sorting algorithms in Java. VSTTE'17?
-
https://github.com/KeYProject/TimSort
TimSort -- also a JDK default sorting algorithm. CAV'15. Bug found.
-
https://github.com/KeYProject/verifythis-ltc-2020
Simplified Version of the Hagrid key-server
-
https://github.com/wadoon/key-citool
A helper to prove Java+JML Programs inside CI pipelines
-
https://github.com/wadoon/smt2key
Translate an SMT file into a KeY file, as best as possible.
-
https://github.com/wadoon/key-tacletdoc
Generation of documentation for KeY files. Generated documentation can be found here
-
https://github.com/wadoon/pygments-jml-key
Syntax highlighting for JML and KeY files for the pygments (Python) system.
-
https://github.com/ekuiter/KeYPR
Proof Repository with KeY
-
https://github.com/KIT-TVA/CorC
Correctness-by-Construction using the KeY Theorem Prover
-
https://github.com/wadoon/key-interactionlog
A plugin that can log your interaction with KeY for documentation, replay or scripting reasons.
-
https://github.com/jmltoolkit/jmlparser
From source code to AST with support for Java 21+ and JML annotation.