Curriculum M1 MPRI at ENS Paris-Saclay

IVER: Introduction to Verification

Description: The course provides an introduction to model-checking techniques used to verify the reliability of critical systems. It begins with the modeling of discrete-event systems—transition systems augmented with data structures for communication (variables, messages) and various synchronization methods. Next, we examine temporal logics (linear and branching-time) for expressing properties to be verified, specifically LTL, CTL, and CTL*. We study their expressiveness, decidability, and the complexity of associated problems.

The second part of the course focuses on advanced methods to address the state-space explosion problem. In particular, we cover Binary Decision Diagrams (BDDs), partial-order reduction, and counterexample-guided abstraction refinement, as well as the concepts of simulation and bisimulation. While the majority of the course deals with the verification of finite-state systems, we also introduce model checking for infinite-state systems by studying Petri nets and pushdown automata.

Summary:

  1. Modeling (transition systems, variables, channels, synchronization)
  2. Linear and branching logics, expressiveness
  3. Büchi automata, LTL translation
  4. Model-checking algorithms for CTL, bisimulation
  5. Emptiness testing for Büchi automata, on-the-fly model checking
  6. Partial-order reduction, application to LTL
  7. Binary Decision Diagrams (BDDs), application to CTL
  8. Verification of pushdown automata
  9. Petri nets (bounded and unbounded)
  10. Abstraction and refinement


References:

  • Christel Baier and Joost-Pieter Katoen. Principles of Model Checking, MIT Press 2008
  • Web site of instructors ...