Hide menu

TDDE34 Software Verification

Preliminary Plan

Course timetable can be found in timedit. Follow a description of the course progression with links to lectures.

Explicit Model Checking
Lecture 1 (fo01.pdf)

[V13] Tis 30/03: Course organization. Introduction to verification, Model Checking and Temporal Logic

Lecure 2 (fo02.pdf)

[V13] Ons 31/03: Büchi acceptance. Explicit model checking. Spin.

Tutorial1 (based on lectures 1 and 2)

[V14] Tis 06/04: Temporal logic. Spin.

Lab (uppg1.pdf)

[V14] Ons 07/04


[V14] Fre 09/04

Symbolic verification
Lecure 3 (fo03.pdf)

[V15] Ons 14/04: Binary Decision Diagrams, Sat solvers

Lecure 4 (fo04.pdf)

[V15] Tor 15/04: Satisfiability Modulo Theory. Symbolic execution.

Tutorial 2 (applications of lectures 3 and 4)

[V15] Fre 16/04: NuSMV, KLEE

Lab (uppg2.pdf)

[V16] Tis 20/04


[V16] Ons 21/04


[V16] Fre 23/04

Axiomatic reasoning
Lecure 5 (fo05.pdf)

[V17] Tis 27/04

Hoare logic. Weakest preconditions. Invariants.

Lab (uppg3.pdf)

[V17] Ons 28/04

Lecure 6 (fo06.pdf)

[V18] Tis 04/05: Cont. Verification of vs. partial total correctness. Dafny.


[V18] Ons 05/05


[V18] Fre 07/05

Abstraction and over-approximations
Lecure 7 (fo07.pdf)

[V19] Mon 10/05: Introduction to Abstract interpretation.

Lecure 8 (fo08.pdf)

[V19] Tis 11/05: Introduction to Predicate abstraction.

Lab (uppg4.pdf)

[V19] Ons 12/05


[V20] Ons 17/05


[V20] Tis 18/05


[V20] Ons 19/05

Lecure 9

[V21] Tis 25/05: Discuss an old exam and a possible solution.


June 4th kl 14-18. Do not forget to register to the exam (2021-05-05 - 2021-05-25). No drop-in! See exam time here.

Page responsible: Ahmed Rezine
Last updated: 2021-05-24