Category: Announcement

KeY 3.0

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

KeY Tutorial @ FM 2024

At FM 2024 in Milan, participants had the opportunity to take part in a tutorial about the KeY system. The tutorial was designed to be accessible for newcomers to formal methods but also to provide value for those with some experience in formal methods (but not KeY itself). The tutorial offered a structured introduction to deductive verification using a combinination of conceptual explanation with hands-on exercises.

Continue reading “KeY Tutorial @ FM 2024” →