Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 5: introduction and organization, logic and proving.
- October 12: the RISC ProofNavigator, specifying and verifying (part 1).
- October 19: specifying and verifying (part 2).
- November 9: compositional approach for program specification and verification (Nikitchenko).
- November 13 (15:30-18:45, T 642): compositional approach for program specification and verification (Nikitchenko).
- November 16: compositional approach for program specification and verification (Nikitchenko).
- November 23: specifying and verifying (part 3), the RISC ProgramExplorer (part 1).
- November 30: the RISC ProgramExplorer (part 2), JML (part 1).
- December 7: ESC/Java 2.
- December 14: The Key Verifier, JML (part 2).
- January 11: modeling concurrent systems, specifying in temporal logic (part 1).
- January 18: specifying in temporal logic (part 2), the Spin model checker.
- January 25: automatic model checking.
- February 1: Exam