Materials
Section outline
-
Thinking Programs (draft manuscript, password will be handed out in class)
Chapter 8: Computer Programs (teaser pages only)
- 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)
- Formally Verified Software in the Real World (restricted)
- Formal Methods in Dependable Systems Engineering (local copy)
- Demonstration Examples
- Logic, Checking, and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- Assigning Meaning to Programs (restricted)
- An Axiomatic Basis for Computer Programming (restricted)
- summation.txt, linsearch2.txt, linsearch3.zip
- 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
The password to this area is handed out in class.