Semantics and Verification

Course of the M1 in Computer Science, ENS de Lyon.

• Tuesday 08:00 - 10:00 10:15 - 12:15, Amphi E.
• Tutorials by Lison Blondeau-Patissier.
• This course in the Portail des études.

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
• Linear-Time Properties
  • Definition and Examples
  • Characterizations via Order Theory and Topology
  • Linear Temporal Logic
  • ω-Regular Properties and Büchi Automata
• Bisimulation and Modal Logic
  • Bisimulation and Trace Equivalence
  • Hennessy-Milner 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 24th of February 2025 10th of March 2025 (see instructions inside).
• Part II to be completed for the 10th of March 2025 17th of March 2025 (see instructions inside).

Final Exam

• Allowed documents: handwritten or typeset course notes. No article. No book.

Courses

• Course 1 (Jan. 14th)
  • 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).

• Course 2 (Jan. 21st)
  
  • Linear-Time Properties:
    • General definitions and Examples.
    • Safety properties (beginning).

• Course 3 (Jan. 28th)
  
  • Linear-Time Properties:
    • Safety properties (Kőnig's Lemma and Characterization of Trace-Equivalence).
    • Liveness properties.
    • The Decomposition Theorem.
  • Topological Approach:
    • Generalities.
    • The Topological Decomposition Theorem.
    • The Space of ω-Words.

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

• Course 5 (Feb. 11th)
  
  • Observable Properties.
  • The Logic LML (beginning).
  • Introduction to the Homework.

• Course 6 (Feb. 18th)
  
  • LML and Observable Properties.
  • Extending LML with Fixpoints.

• Course 7 (Feb. 25th)
  • The Logic LTL.
  • ω-Regular Properties (§4.3 of the book):
    • ω-Regular Expressions (§4.3.1).
    • Non-Deterministic Büchi Automata (NBAs) (§4.3.2).
    • NBAs and ω-Regular Expressions (§4.3.2).

• Course 8 (Mar. 11th)
  • ω-Regular Properties (§4.3 of the book):
    • 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 (Mar. 18th).
  • Translation of LTL to (G)NBA's (§5.2 of the book).
  • LTL vs NBAs (§5.2 of the book).
  • Bisimulation.

• Course 10 (Mar. 24th).
  • Modal Logics of Transition Systems:
    • The Hennessy-Milner Property.
    • Modal Saturation.
    • Boolean Algebras with Operators.
    • Ultrafilter Extensions of Kripke Models.

Back home.