Section outline

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

    1. October 5: introduction and organization, the language of logic, the RISC Algorithm Language.
    2. October 12: specifying and verifying (part 1).
    3. October 19: specifying and verifying (part 1).
    4. November 5 (10:15-13:30, S3 048): exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
    5. November 7 (15:30-18:45, K 001A):  Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
    6. November 9: modeling tools, retrial queueing systems, case studies. (Sztrik).
    7. November 16: specifying and verifying (part 1), the art of proving, the RISC ProofNavigator,
    8. November 23: specifying and verifying (part 2), the RISC ProgramExplorer.
    9. November 30: JML (part 1), ESC/Java2.
    10. December 7: ESC/Java2, the Key Verifier.
    11. December 14: JML (part 2), modeling concurrent systems.
    12. January 11: specifying in temporal logic.
    13. January 18: the Spin model checker.
    14. January 25: automatic model checking, verifying safety properties by computer-supported proving.