Formal Verification -- M1 ENS Saclay (2024--2025)

News

Plan

• Introduction to the formal verification.
  
• Formal models to represent the behaviour of reactive systems.
  
• Temporal logics for the specification avec verification
  
  
  • Linear Time Temporal Logic (LTL): definitions, examples, expressivity, decision procedures.
    
  • Computation Tree Logic (CTL): definitions, examples, expressivity, decision procedures.
    
  • Extensions of LTL/CTL
    

Contents of the lectures

• 1st lecture (20/09) : Introduction to the formal verification; Definition of Kripke structures; LTL (syntax, semantics, example).
• 2nd lecture (27/09) : Expressivity of LTL fragments (notions of equivalence, Separation Theorem; Comparison of L(U,X,S,X-1) and L(U,X), L(U,X) and L(F,X), L(U,X) and L(U), L(F,X) and L(X).
• 3rd Lecture (4/10) : Introduction to Büchi automata. Construction of the automaton which recognizes the models of a given L(X,U) formula.
• 4th Lecture: correctness of the automata construction; complexity of verification problems for LTL; introduction to CTL.
• 5th Lecture: CTLM model-checking algorithm; CTL and strong bisimulation.

Documents

• Slides of the 1st lecture: here.
  
• An emergency kit for LTL: here.
  
• An emergency kit for CTL: here.
  
• Notes about S1S: here.
  
  

Biblio.

Email: francoisl[at]irif.fr