 Tutorials by Henning Basold. The tutorials' page is here.

The course closely follows the book:
 Baier, C. and Katoen, J.P., Principles of Model Checking, MIT Press, 2008.
Overview
The goal of formal verification is to check automatically that some programs or systems
are correct with respect to their requirements.
In this course we present mathematical models of programs and systems
and we
describe classes of properties which can be automatically checked on these models.
Content of the course:
 Modelling with Labelled Transition Systems
 LinearTime Properties
 Definition and Examples
 Characterizations via Order Theory and Topology
 ωRegular Properties and Büchi Automata
 Linear Temporal Logic
 Bisimulation and Modal Logic
 Bisimulation and Trace Equivalence
 HennessyMilner Logic
 Bisimulation and Logical Equivalence
Prerequisites:

We assume some familiarity with automata theory and mathematical logic,
essentially
corresponding to the courses Fondements de l'informatique and Logique given in the
L3 year of the Computer Science Department of the ENS de Lyon.
Courses

Course 1 (Jan. 30th)
 General overview of the course.
 Modelling Concurrent Systems (part. 1).

Course 2 (Feb. 4th)
 Modelling Concurrent Systems (part. 2).

LinearTime Properties:
 General definitions and Examples.

Course 3 (Feb. 11th)

LinearTime Properties:
 Safety.
 Liveness.

LinearTime Properties:

Course 4 (March 4th)

LinearTime Properties:
 Fairness assumptions.

Regular Properties:
 Regular Safety.
 ωRegular expressions.

LinearTime Properties:

Course 5 (March, 11th)
 NonDeterministic Büchi Automata (NBAs).
 NBAs and ωRegular Expressions.
 Deterministic Büchi Automata (DBAs).

Course 6 (March, 18th)
 Generalized Büchi automata (GNBAs) and closure under intersection of ωregular languages.

Linear Temporal Logic (LTL):
 Syntax and Semantics.

Course 7 (March, 25th)

Linear Temporal Logic (LTL):
 Translation to (Generalized) Büchi automata.
 Positive Normal Forms.

Linear Temporal Logic (LTL):

Course 8 (April, 1st)

HennessyMilner Logic and Bisimulation.

Bisimulation:
 Definition and Examples.
 Bisimilarity and Trace Equivalence.

HennessyMilner Logic:
 Definition.
 Bisimilarity implies Logical Equivalence.
 Modal Saturation.
 Modal Saturation by Ultrafilter Extensions (beginning).

Bisimulation:

HennessyMilner Logic and Bisimulation.

Course 9 (April, 8th)

HennessyMilner Logic and Bisimulation.
 Modal Saturation by Ultrafilter Extensions (end).
 EhrenfeuchtFraïssé method for undefinability (beginning).

HennessyMilner Logic and Bisimulation.

Course 10 (April, 9th)
 EhrenfeuchtFraïssé method for undefinability.
Back home.