KeY
Published:
The core feature of KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus. It allows for full functional verification of sequential Java (without floats, garbage collection and multithreading) and Java Card 2.2.x programs. Properties can be specified in the Java Modelling Language (JML) or in Java Dynamic Logic directly. (from key-project.org)
KeY is a long-running international project in software verification, and I contributed to it by implementing Nathan Wasser’s approach to loop invariant inference in 2013-2016.