Schedule

Lectures in italics are mandatory for KV4 students but recommended also to KV3 students.

1. October 14: introduction and organization, the language of logic.
2. October 21: the art of proving, the RISC ProofNavigator.
3. October 28: specifying and verifying (part 1).
4. November 4: specifying and verifying (part 1).
5. November 11: specifying and verifying (part 2), the RISC ProgramExplorer.
6. November 18: specifying and verifying (part 2).
7. November 25: JML (part 1), ESC/Java 2.
8. December 2: ESC/Java 2, the KeY verifier.
9. December 9: JML (part 2).
10. December 16: modeling concurrent systems.
11. January 13: specifying in temporal logic (part 1), the Spin model checker.
12. January 20: specifying in temporal logic (part 2).
13. January 27: automatic model checking.
14. February 3: Exam