Section outline

  • The schedule is tentative and may be modified.

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

    1. October 9: introduction and organization, logic and proving.
    2. October 16:  the RISC ProofNavigator, specifying and verifying (part 1).
    3. October 23: specifying and verifying (part 2).
    4. October 30: specifying and verifying (part 3), the RISC ProgramExplorer.
    5. November 6: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
    6. November 10 (8:30-11:45, S2 Z74):  Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
    7. November 13: modeling tools, retrial queueing systems, case studies. (Sztrik).
    8. November 20: the RISC ProgramExplorer.
    9. November 27: JML (part 1), ESC/Java2.
    10. December 4: ESC/Java2, the Key Verifier.
    11. December 11: JML (part 2), modeling concurrent systems.
    12. December 18: specifying in temporal logic.
    13. January 15: the Spin model checker.
    14. January 22: automatic model checking.