Swedish web site
TDDE34 Software Verification
Plan for the lectures and the lessons
| Explicit Model Checking | |
|
Lecture 1: Course organization. Introduction to verification, Model Checking and Temporal Logic. |
(temporal-1.pdf) |
|
Lecture 2: Büchi acceptance. Explicit model checking. Spin. |
(temporal-2.pdf) |
|
Tutorial 1: based on lectures 1 and 2 with discussions on temporal logic and Spin. |
|
| Axiomatic reasoning | |
|
Lecture 3: Hoare logic. Weakest preconditions. Invariants. |
(partial.pdf) |
Lecture 4: Cont. Verification of vs. partial total correctness. Dafny. |
(total.pdf) |
| Symbolic verification | |
|
Lecture 5:Sat solvers, by guest researcher Johannes K. Fichte |
(sat.pdf) |
| Lecture 6: Satisfiability Modulo Theory. Symbolic execution. |
(smt.pdf) |
|
Tutorial 2: based on lectures 5 and 6 with discussions of NuSMV and KLEE. |
|
| Abstraction and over-approximations | |
|
Lecture 7:Introduction to Abstract interpretation. |
(ai.pdf) |
|
Lecture 8: Introduction to Predicate abstraction. |
(pa.pdf) |
| Recapitulation, exam discussion |
Page responsible: Ahmed Rezine
Last updated: 2026-03-23
