Just in time for the 22th KeY Symposium, we are very happy to present the new 3.0 release of KeY. You can download it from GitHub.
Most importantly, this major 3.0 release is now based on JavaParser instead of Recoder, which opens the path for supporting modern Java. At the moment, support for records and text block literals is already implemented. Further exciting new features are: Support for polymorphic sorts and functions in KeY’s logic, a modularized internal structure that allows for development of verifiers for different target languages (such as Rust in RustyKeY and Solidity in KeYther), and proof scripts that can be written in JML directly into the source file.
There are many more new features, improvements, and bug fixes, a full changelog can be found at the release page.
Thanks to all developers and testers for your efforts!
The KeY Team
