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

Lecture 2: Büchi acceptance. Explicit model checking. Spin.

Tutorial 1: based on lectures 1 and 2 with discussions on temporal logic and Spin.

Lecture 3:Binary Decision Diagrams, Sat solvers

Lecture 4: Satisfiability Modulo Theory. Symbolic execution.

Tutorial 2: based on lectures 3 and 4 with discussions of NuSMV and KLEE.

Lecture 5: Hoare logic. Weakest preconditions. Invariants.

Lecture 6: Cont. Verification of vs. partial total correctness. Dafny.

Lecture 7:Introduction to Abstract interpretation.

Lecture 8: Introduction to Predicate abstraction.