Section outline

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

    1. October 5: introduction and organization, logic and proving.
    2. October 12:  the RISC ProofNavigator, specifying and verifying (part 1).
    3. October 19: specifying and verifying (part 2).
    4. November 9: compositional approach for program specification and verification (Nikitchenko).
    5. November 13 (15:30-18:45, T 642): compositional approach for program specification and verification (Nikitchenko).
    6. November 16: compositional approach for program specification and verification (Nikitchenko).
    7. November 23: specifying and verifying (part 3), the RISC ProgramExplorer (part 1).
    8. November 30: the RISC ProgramExplorer (part 2), JML (part 1).
    9. December 7: ESC/Java 2.
    10. December 14: The Key Verifier, JML (part 2).
    11. January 11: modeling concurrent systems, specifying in temporal logic (part 1).
    12. January 18: specifying in temporal logic (part 2), the Spin model checker.
    13. January 25: automatic model checking.
    14. February 1: Exam