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.
The session was divided into two parts. The first part focused on introducing the principles behind KeY, including its foundation in dynamic logic and the use of the Java Modeling Language (JML) for specifying software behavior. Along concrete examples, the presenters walked participants through the basic workflow of verifying Java code against formal contracts, demonstrating how symbolic execution and proof rules are applied in practice.
The second part of the tutorial was a guided hands-on session. Participants worked with the KeY tool. They specified and verified Java programs on their own, but with members of the KeY team available to assist when necessary.
We hope the participants enjoyed the experience as much as we did.
You can find links to all materials here.
