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 from the L3 year of the Computer Science Department of ENS de Lyon:
 Fondements de l'informatique.
 Logique.
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 7th of March 2023 (see instructions inside).

Part II
to be completed for the
21st of March28th of March 2023 (see instructions inside).
Final Exam
 Allowed documents: handwritten or typeset course notes. No article. No book.
Courses

Course 1 (Jan. 11th)

General overview of the course.
 See Chap. 1 of the book for an informal introduction to verification (up to 2008).
 Modelling Concurrent Systems (Chap. 2 of the book).

General overview of the course.

Course 2 (Jan. 18th)

LinearTime Properties:
 General definitions and Examples.
 Safety properties.

LinearTime Properties:

Course 3 (Jan. 25th)

LinearTime Properties:
 Liveness properties.
 The Decomposition Theorem.

Topological Approach:
 Generalities.
 The Topological Decomposition Theorem.
 Spaces of ωWords.

LinearTime Properties:

Course 4 (Feb. 1st)
 Partial Orders, Complete Lattices, Closure Operators and Galois Connections.

Course 5 (Feb. 8th)
 Observable Properties.
 The Logic LML (introduction).

Course 6 (Feb. 22nd)
 The Logic LML.
 Introduction to the Homework.
 Extending LML with Fixpoints.

Course 7 (March 1st)
 The Logic LTL.

ωRegular Properties
(§4.3 of the book):
 ωRegular Expressions (§4.3.1).
 NonDeterministic Büchi Automata (NBAs) (§4.3.2).

Course 8 (March 8th)
 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).
 Translation of LTL to (G)NBA's (§5.2 of the book).

Course 9 (March 22nd).
 Bisimulation.
 Modal Logics of Transition Systems (beginning).

Course 10 (March 29th).

Modal Logics of Transition Systems:
 The HennessyMilner Property.
 Modal Saturation.
 Boolean Algebras with Operators.
 Ultrafilter Extensions of Kripke Models.

Modal Logics of Transition Systems:
Back home.