DD2452 Formal
Methods
-
Course Outline -
- Introduction to Formal Methods
- Course syllabus
- Course organization
Part
I: Hoare
Logic and Program Verification
Class 2
- Motivation for program specification and verification [book 4.1]
- A core programming language [book 4.2.1]
- Hoare triples [book 4.2.2]
- Partial and total correctness [book 4.2.3]
- Hoare triples vs (partially) annotated programs
Class 3
- Program variables and logical variables [book 4.2.4, Exercises
4.2]
- A proof calculus for partial correctness [book 4.3.1]
Class 4
- Loop invariants [book 4.3.2]
- Proof tableaux [book 4.3.2]
- Example verifications [book 4.3.2, Exercises 4.3]
Class 5
- Weakest preconditions and automatic verification
- Assignment 1: (see
assignments page)
Class 6
- Peer assessment of Assignment 1
- Brief introduction to ESC/Java [slides]
[book 4.5]
Class 7
Class 8
- A proof calculus for total correctness [book 4.4, Exercises 4.4]
Classes 9-10
- A proof calculus for concurrent programs [slides]
- Assignment 2: (see
assignments page)
Part II:
Temporal Logic and Model
Checking
Class 11
- Peer assessment of Assignment 2
- Introduction to model checking [book 3.1]
Class 12
- Linear-time Temporal Logic (LTL) [book 3.2, 3.8: Exercises 3.2] [handout]
- Assignment 3: (see
assignments page)
Class 13
- Peer assessment of Assignment 3
- Model checking: An automata based approach
Class 14
- LTL model checking [book 3.6.3]
- SPIN lab assignment presentation [text]
- Assignment 4: (see
assignments page)
Class 15
- Introduction to the Protocol Meta Language (Promela) [slides]
Class 16
- Peer assessment of Assignment 4
- Computation Tree Logic (CTL) [book 3.4] [handout]
- Course Summary
- Exam Preparation
- Course Evaluation [form]