 BBB classroom.
 Tutorials by Christophe Lucas. The tutorial page is here.
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 ENS de Lyon.
Bibliography:
 Course notes [pdf] (regularly updated).
 The course is mostly based on the book:
 Baier, C. and Katoen, J.P., Principles of Model Checking, MIT Press, 2008.
Homework
 The homework in [pdf].
 Part I to be completed for the 2nd of March 2021 (see instructions inside).
 Part II to be completed for the 16th of March 2021 (see instructions inside).
Courses

Course 1 (Jan. 6th)
[scan]
 General overview of the course.
 Modelling Concurrent Systems (Chap. 2 of the book).

Course 2 (Jan. 20th)
[scan]
[recording]

LinearTime Properties:
 General definitions and Examples.
 Safety (beginning).

LinearTime Properties:

Course 3 (Jan. 27th)

Course 4 (Feb. 3rd)

Course 5 (Feb. 10th)

Course 6 (Feb. 24th)

Course 7 (March 3rd)
[scan]
(§4.3 of the book)
 ωRegular expressions (§4.3.1).
 NonDeterministic Büchi Automata (NBAs) (§4.3.2).
 NBAs and ωRegular Expressions (§4.3.2).
 Deterministic Büchi Automata (DBAs) (§4.3.3).
 Generalized Büchi automata (GNBAs) and closure under intersection of ωregular languages (§4.3.4).
 Course 8 (March 10th)
 Course 10 (March 2th).
Back home.