Schedule

The following is a preliminary schedule of the lecture:

1. October 9: introduction and organization, the language of logic. 
2. October 16: the RISC Algorithm Language, specifying and verifying.
3. October 23: specifying and verifying.
4. October 30: specifying and verifying.
5. November 6: the art of proving, the RISC Theorem Proving Interface.
6. November 13: specifying and verifying.
7. November 20: the Java Modeling Language (part 1).
8. November 27:  extended static checking of Java programs with ESC/Java2.
9. December 4: verifying Java programs with KeY.
10. December 11: the Java Modeling Language (part 2).
11. December 18: modeling concurrent systems.
12. January 8:  specifying in temporal logic, verifying safety properties.
13. January 15: the Spin model checker, automatic model checking.
14. January 22: (no lecture)
15. January 29: exam