Section outline

  • The following is a preliminary schedule of the lecture:

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