Formal Analysis of Java Programs with KeY - Exercise Material

Slides: Lecture 1, Lecture 2
Browse or download the examples from the lectures as well as additional ones. The examples are sorted according to the topic they cover.
Lab exercises and auxiliary material
Draft of the KeY-Cheat Sheet with an overview about the KeY Syntax.
Interpreting not-closeable proofs: a case study based on the Zune 30 GB New Years Bug

Attention: You find the KeY version used in the lecture and for the lab here. Please do not use another version.

Last modified: Wed Jan 28 08:21:43 CET 2009