Schedule

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.