## 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]