Lecture 1 (fo01.pdf)

Course organization. Introduction to verification, Model Checking and Temporal Logic

Lecure 2 (fo02.pdf)

Büchi acceptance. Explicit model checking. Spin.

Tutorial1 (based on lectures 1 and 2)

Temporal logic. Spin.

Lab (uppg1.pdf)

Lab

Lecure 3 (fo03.pdf)

Binary Decision Diagrams, Sat solvers

Lecure 4 (fo04.pdf)

Satisfiability Modulo Theory. Symbolic execution.

Tutorial 2 (applications of lectures 3 and 4)

NuSMV, KLEE

Lab (uppg2.pdf)

Lab

Lab

Lecure 5 (fo05.pdf)

Hoare logic. Weakest preconditions. Invariants.

Lab (uppg3.pdf)

Lecure 6 (fo06.pdf)

Cont. Verification of vs. partial total correctness. Dafny.

Lab

Lab

Lecure 7 (fo07.pdf)

Introduction to Abstract interpretation.

Lecure 8 (fo08.pdf)

Introduction to Predicate abstraction.

Lab (uppg4.pdf)

Lab

Lab

Lab

Lesson

Discuss an old exam and a possible solution.