Section outline

  • The following is a preliminary schedule of the lecture:

    1. October 8: introduction and organization, the language of logic.
    2. October 15: the RISC Algorithm Language, specifying and verifying (part 1).
    3. October 22: specifying and verifying (part 1).
    4. October 29: specifying and verifying (part 1).
    5. November 5: the art of proving, the RISC ProofNavigator.
    6. November 12: specifying and verifying (part 2), the RISC ProgramExplorer.
    7. November 19: the Java Modeling Language (part 1).
    8. November 26: the extended static checking of Java programs with ESC/Java2.
    9. December 3: verifying Java programs with KeY.
    10. December 10: the Java Modeling Language (part 2),
    11. December 19: modeling concurrent systems.
    12. January 7: specifying in temporal logic.
    13. January 14: the Spin model checker, automatic model checking.
    14. January 21: automatic model checking, verifying safety properties by proving.