Materials
Section outline
-
- Computer Programs/Systems as Subject of Formal Reasoning
- Introduction (4 on 1)
- Fehler im System: der Traum von Software ohne Bugs (restricted)
- Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
- Formal Methods: Practice and Experience (local copy)
- Demonstration Examples
- Logic and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- Specifying and Verifying Programs: Part 2 (4 on 1)
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- Behavioral Interface Specification Languages (restricted)
- Specification and Verification: The Spec# Experience (restricted)
- Extended Static Checking with ESC/Java 2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Specifying and Verifying Concurrent Systems
- Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
The password to this area is handed out in class.