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)
- Proof of Correctness of Data Representations (restricted)
- Formal Verification of Object-Oriented Software (COST Action IC0701)
- Demonstration Examples
- Specifying and Verifying Concurrent Systems
- Modeling Concurrent Systems (4 on 1)
- Specifying and Verifying System Properties (4 on 1)
- Model-Checking Concurrent Systems (4 on 1)
- Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
- Talking Model Checking Technology (restricted)
- ClientServer.txt
- Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
The password to this area is handed out in class.