Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 4: introduction and organization, logic and proving.
- October 11: the RISC ProofNavigator, specifying and verifying (part 1).
- October 18: specifying and verifying (part 2).
- November 8: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 12 (15:30-18:45, S2 048): Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 15: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 22: specifying and verifying (part 3), the RISC ProgramExplorer.
- November 29: the RISC ProgramExplorer.
- December 6: JML (part 1), ESC/Java2.
- December 13: ESC/Java 2, the Key Verifier.
- January 10: JML (part 2), modeling concurrent systems.
- January 17: specifying in temporal logic.
- January 24: the Spin model checker.
- January 31: automatic model checking.