Schedule

The following is a preliminary schedule of the lecture:

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