Section outline

  • Schedule
    1. October 10: introduction, logic, RISC ProofNavigator.
    2. October 17: RISC ProofNavigator, Hoare calculus.
    3. October 24: Hoare calculus, verification with RISC ProofNavigator.
    4. October 31 (T111!): Hoare calculus, verification with RISC ProofNavigator.
    5. November 7 (KV4): Queuing theory and its applications (Sztrik).
    6. November 10 (KV4, HS13/HS14): Queuing theory and its applications (Sztrik).
    7. November 14 (KV4): Queuing theory and its applications (Sztrik).
    8. November 21: JML (part 1), ESC/Java2.
    9. November 28: ESC/Java2, KeY.
    10. December 5: JML (part 2).
    11. December 12: modeling concurrent systems, simulating with Spin.
    12. December 19: specifying concurrent systems.
    13. January 9: model checking concurrent systems with Spin.
    14. January 16: verifying concurrent systems with the RISC ProofNavigator.
    15. January 30: exam.