Materials

• 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)
• Demonstration Examples
• Specifying and Verifying Sequential Programs
• Specifying and Verifying Programs: Part 1 (4 on 1)
• An Axiomatic Basis for Computer Programming (restricted)
• Specifying and Verifying Programs: Part 2 (4 on 1)
• Demonstration Examples
• Invariant-based Programming
• Paper (local copy)
• Dutch National Flag
• Specifying and Verifying Java Programs
• The Java Modeling Language: Part 1 (4 on 1)
• Extended Static Checking with ESC/Java 2 (4 on 1)
• Demonstration Examples
• Verifying Java Programs with KeY (4 on 1)
• Demonstration Examples
• 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 Properties of Concurrent Systems (4 on 1)
• Demonstration Examples
• Model-Checking Concurrent Systems (4 on 1)
• Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
• Talking Model Checking Technology (restricted)
• Demonstration Examples

Restricted Area

The password to this area is handed out in class.