Section outline

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

    1. October 4: introduction and organization, logic and proving.
    2. October 11:  the RISC ProofNavigator, specifying and verifying (part 1).
    3. October 18: specifying and verifying (part 2).
    4. November 8: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
    5. 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).
    6. November 15: modeling tools, retrial queueing systems, case studies. (Sztrik).
    7. November 22: specifying and verifying (part 3), the RISC ProgramExplorer.
    8. November 29: the RISC ProgramExplorer.
    9. December 6: JML (part 1), ESC/Java2.
    10. December 13: ESC/Java 2, the Key Verifier.
    11. January 10: JML (part 2), modeling concurrent systems.
    12. January 17: specifying in temporal logic.
    13. January 24: the Spin model checker.
    14. January 31: automatic model checking.