Section outline

  • Schedule
    Lectures marked as "KV4" are mandatory for KV4 students but also recommended for KV3 students.
    1. October 15: Introduction, the language of logic.
    2. October 22: RISC ProofNavigator, Hoare calculus.
    3. October 29: Hoare calculus, verification with the RISC ProofNavigator.
    4. November 5 (Sztrik): Exponential distribution and its properties, Poisson process, Markov Chains, etc.
    5. November 10 (Sztrik, T111+T211): Markov-type Queueing Systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations.
    6. November 12 (Sztrik): Modeling tools, Retrial Queueing Systems, Case Studies.
    7. November 19: Hoare calculus, verification with the RISC ProofNavigator.
    8. November 26: JML (part 1), ESC/Java2.
    9. December 3: ESC/Java2, KeY.
    10. December 10: JML (part 2).
    11. December 17: modeling concurrent systems, simulating with Spin.
    12. January 14: specifying concurrent systems.
    13. January 21: model checking concurrent systems with Spin.
    14. January 28: model checking, verifying concurrent systems with the RISC ProofNavigator.
    15. February 5: exam.