Section outline

  • Schedule
    Lectures marked as "KV4" are mandatory for KV4 students, KV3 students are welcome.
    1. October 9: introduction, the language of logic.
    2. October 16: RISC ProofNavigator, Hoare calculus.
    3. October 23: Hoare calculus, verification with the RISC ProofNavigator.
    4. October 30 (KV4): More on Hoare calculus and verification.
    5. November 13: JML (part 1), ESC/Java2.
    6. November 20: ESC/Java2, KeY.
    7. November 27: JML (part 2).
    8. December 4: modeling concurrent systems, simulating with Spin.
    9. December 11: specifying concurrent systems.
    10. December 18: model checking concurrent systems with Spin.
    11. January 15 (KV4): verifying concurrent systems with the RISC ProofNavigator.
    12. January 22 (KV4): guest lecture cancelled, self study assignment instead.
    13. January 29: February 1: exam.