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

Lab

[V14] Fre 09/04

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

Lab

[V16] Ons 21/04

Lab

[V16] Fre 23/04

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.

Lab

[V18] Ons 05/05

Lab

[V18] Fre 07/05

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

Lab

[V20] Ons 17/05

Lab

[V20] Tis 18/05

Lab

[V20] Ons 19/05

Lecure 9

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

Exam

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.