Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:2012-2013-c-1-22 [2013/10/03 13:57] (current)
gastin created
Line 1: Line 1:
  
 +====== Basics of Verification (48h, 6 ECTS) ======
 +
 +
 +In charge: [[http://www.lsv.ens-cachan.fr/~gastin/|Paul Gastin]] (LSV, ENS Cachan).
 +
 +====== Lecturers ======
 +
 +[[http://www.lsv.ens-cachan.fr/~gastin/|Paul Gastin]] (lectures), 
 +[[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]] (lectures), 
 +[[http://www.lsv.ens-cachan.fr/~schmitz/|Sylvain Schmitz]] (exercises).
 +
 +/*
 +---++ Research internships
 +
 + 1 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Synthesis of Distributed Real-Time Systems]]
 + 1 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Dynamic Communicating Automata]]
 + 1 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Quantitative versus Probabilistic Logics]]
 + 1 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Temporal Logic for Concurrent Recursive Programs]]
 + 1 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Quantitative properties of trees. Application to XML query languages]]
 +*/
 +
 +====== Language ======
 +
 +
 +The default language is French.\\
 +But the lectures may be given in English if attended by non French-speaking students.
 +
 +====== Motivations and main objectives ======
 +
 +
 +Nowadays, it is of the highest importance to use formal methods in order to increase the reliability of critical systems.
 +\\
 +In this introductory course on verification of discrete systems, we concentrate in particular on _model checking_ techniques.
 +\\
 +We will describe various models used to define systems: transition systems enriched with various data structures (variables, channels, ...) and which can be composed with several synchronization mechanisms.
 +\\
 +We will also cover specification languages that are used to express properties to be checked on our systems: temporal logics (linear or branching), first-order or monadic second-order logic, ...
 +\\
 +We will study expressivity, decidability and complexity properties of our models and specification languages.
 +\\
 +We will also cover abstraction/refinement techniques and (bi)simulation relations used to relate various abstraction levels.
 +\\
 +Algorithmic aspects of model checking will be investigated and we will stress efficient techniques such as binary decision diagrams (BDDs) or bounded model checking.
 +/*
 +Pour cela nous introduirons divers modèles d'automates sur les mots infinis (Büchi, Muller, parité, ...) et aussi alternants.
 +*/
 +
 +====== Detailed description and Lecture notes ======
 +
 +The full lecture notes of the first half of the semester are available [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-4up.pdf|here]].
 +
 +| **Date** | **Type** | **Topics covered** |
 +| **2012/09/19** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-lecture1-4up.pdf|Lecture]] | Introduction \\ Models: transition systems, variables, synchronized products, Rendez-vous, shared variables, atomicity, asynchronous communication with channels |
 +| **2012/09/26** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td01.pdf|Exercises]] | Mutual exclusion algorithms, Handshake with data exchange, Needham-Schroeder protocol, Channel systems|
 +| **2012/10/03** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-lecture2-4up.pdf|Lecture]] | Specification: introduction, linear vs branching specifications, FO and TL: definitions and examples, linear model checking, branching specifications, MSO, CTL<sup>*</sup> |
 +| **2012/10/10** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td02.pdf|Exercises]] | Temporal Logics: LTL, CTL<sup>*</sup>, CTL, CTL<sup>+</sup>|
 +| **2012/10/17** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-lecture3&4-4up.pdf|Lecture]] | CTL, PTIME model checking algorithm for CTL and for fair-CTL \\ Büchi automata |
 +| **2012/10/24** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td03.pdf|Exercises]] | CTL model-checking, Büchi automata |
 +| **2012/10/31** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-lecture3&4-4up.pdf|Lecture]] | Büchi transducers: definitions, examples and main properties \\ Construction of a Büchi transducer from an LTL formula \\ Satisfiability and Model checking for LTL: decidability and complexity \\ PSPACE model checking algorithm for CTL<sup>*</sup> \\  |
 +| **2012/11/07** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td04.pdf|Exercises]] | LTL model-checking and complexity |
 +| **2012/11/14** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-12-lecture5-4up.pdf|Lecture]] | Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation |
 +| **2012/11/21** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td05.pdf|Exercises]] | EF Games, Separation |
 +| **2012/12/13** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/c1.pdf|Lecture]] | Petri Nets I |
 +| **2012/12/19** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td06.pdf|Exercises]] | Petri nets: model-checking, unfoldings, VASS |
 +| **2013/01/09** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/c2.pdf|Lecture]] | Petri Nets II  |
 +| **2013/01/16** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td07.pdf|Exercises]] | Coverability |
 +| **2013/01/23** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/c3.pdf|Lecture]] | Binary Decision Diagrams |
 +| **2013/01/30** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td08.pdf|Exercises]] | BDDs |
 +| **2013/02/06** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/c4.pdf|Lecture]] | Pushdown systems |
 +| **2013/02/13** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td09.pdf|Exercises]] | Pushdown systems |
 +| **2013/02/20** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/c5.pdf|Lecture]] | Partial-order reduction |
 +| **2013/02/27** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/td10.pdf|Exercises]] | Parial-order reduction |
 +
 +
 +See also [[2011-2012-c-1-22|previous year]].
 +
 +/*
 +
 +| **2011/10/05** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td02.pdf|Exercises]] | Specification, LTL, LTL with past|
 +| **2011/10/19** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td03.pdf|Exercises]] | Ehrenfeucht-Fraïssé Games |
 +| **2011/11/02** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td04.pdf|Exercises]] | Büchi automata and transducers |
 +| **2011/11/16** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td05.pdf|Exercises]] | TL(X), CTL<sup>*</sup>, and CTL|
 +| **2011/12/07** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/c1.pdf|Lecture]] | Petri nets, unfoldings |
 +| **2011/12/07** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/c1.pdf|Lecture]] | Petri nets, coverability graph |
 +| **2012/01/04** \\ **2012/01/11** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td06.pdf|Exercises]] | Petri nets: modeling, model-checking, unfoldings, coverability graphs, and vector addition systems|
 +| **2012/01/18** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/c2.pdf|Lecture]] | Binary decision diagrams |
 +| **2012/01/25** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td07.pdf|Exercises]] | Binary decision diagrams|
 +| **2012/02/01** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/c3.pdf|Lecture]] | Pushdown systems |
 +| **2012/02/08** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td08.pdf|Exercises]] | Pushdown Systems|
 +| **2012/02/15** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/c4.pdf|Lecture]] | Partial-order reductions |
 +| **2012/02/22** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/td09.pdf|Exercises]] | Partial-Order Reduction |
 +*/
 +
 +/*
 +
 +| **Date** | **Type** | **Topics covered** |
 +| **2009/09/14** | Lecture | Introduction, Models: transition systems, variables, synchronized products, Rendez-vous [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_09_Model1_4up.pdf|slides]] \\ Specification: introduction, LTL: definitions and examples [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_09_spec-ltl1_4up.pdf|slides]] |
 +| **2009/09/21** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td01.pdf|Exercises]] | Handshake with data exchange, Needham-Schroeder protocol\\LTL formulae\\Büchi automata|
 +| **2009/09/28** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_09-lecture2_4up.pdf|Lecture]] | Models: shared variables, atomicity, (lossy) channels \\LTL: past modalities, expressivity, model checking, satisfiability \\Büchi automata|
 +| **2009/10/05** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td02.pdf|Exercises]] | Alternating Bit Protocol\\LTL with Past\\Büchi Complementation|
 +| **2009/10/12** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_09-lecture3_4up.pdf|Lecture]] | Efficient construction of a Büchi automaton from an LTL formula\\Correctness of the construction.\\Satisfiability and Model Checking are PSPACE-complete for LTL specifications (upper bound and lower bound)|
 +| **2009/10/19** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td03.pdf|Exercises]] | LTL to Büchi Automata\\Suttering and LTL(U)\\Lower bounds for LTL(U)|
 +| **2009/10/26** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_09_4up.pdf|Lecture]] | Branching time specifications\\PSPACE model checking algorithm for CTL<sup>*</sup>\\PTIME model checking algorithm for CTL\\Fair CTL and its PTIME model checking algorithm|
 +| **2009/11/02** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td04.pdf|Exercises]] | Model Checking a Path\\CTL<sup>*</sup>, CTL, and CTL<sup>+</sup>\\Fair CTL|
 +| **2009/11/09** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td05.pdf|Simple exercises]]\\in preparation for E1 | LTL and Automata\\CTL and CTL<sup>*</sup>\\Model checking LTL(X) is NP-complete|
 +| **2010/01/04** | Lecture ([[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws0910/bmc.pdf|part 1]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws0910/nets.pdf|part 2]]) | Bounded model checking, Petri nets |
 +| **2010/01/11** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td08.pdf|Exercises]] | Modeling with Petri nets\\LTL model checking for Petri nets\\Coverability, Rackoff's algorithm |
 +| **2010/01/18** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws0910/nets2.pdf|Lecture]] | Petri nets |
 +| **2010/01/25** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2009_verif/td09.pdf|Exercises]] | Vector Addition Systems\\Unfoldings: Adequate Partial Orders, LTL Model Checking |
 +-->
 +
 +<!-- 1. Introduction
 + 1. Modélisation de systèmes : structures de Kripke, produits synchronisés d'automates, automates étendus.
 + 1. Spécification de propriétés : logiques temporelles linéaires (LTL) ou arborescentes (CTL, CTL<sup>*</sup>), FO, MSO, mu-calcul, ...
 + 1. Équivalence entre LTL, FO, star-free, apériodique, automates alternants très faibles.
 + 1. Propriétés de sûreté et de vivacité, caractérisations topologiques, caractérisations en logique temporelle linéaire.
 + 1. Satisfaisabilité et model checking : complexité et algorithmique.
 + 1. Model checking symbolique, diagrammes de décisions binaires.
 + 1. Simulation et bi-simulation. Algorithmique.
 + 1. Outils pour la vérification : [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php|ltl2ba]], [[http://www.brics.dk/mona/|mona]], [[http://spinroot.com/spin/whatispin.html|spin]], [[http://www.cs.cmu.edu/~modelcheck/smv.html|smv]] et [[http://nusmv.irst.itc.it/|nusmv]], ...
 +-->
 +
 +
 +<!--
 + ** Pour la première partie, le [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_08_4up.pdf|support de cours]] proposé est une version améliorée des transparents utilisés pour le cours "Basics of Model Checking" de l'école pour jeune chercheur : 6th Summer School on MOdelling and VErifying parallel Processes (MOVEP 2004). Il contient les définitions, théorèmes et constructions présentés dans la première moitié du cours.
 + ** On pourra aussi consulter, un [[http://www.lsv.ens-cachan.fr/~gastin/Verif/si-bang-dg.pdf|chapitre de livre]] qui traite des logiques temporelles LTL, CTL<sup>*</sup> et ETL. Il contient en particulier la traduction de formules LTL en automates de Büchi généralisés.
 + ** Pour la deuxième partie, on pourra consulter le chapitre de livre [[http://www.lsv.ens-cachan.fr/~gastin/Verif/DiekertGastin-FO-07.pdf|"First-order definable languages"]] dans lequel on prouve l'équivalence entre LTL, FO, star-free, aperiodic, counter-free Büchi automata, aperiodic Bûchi automata, very weak alternating automata, ainsi que le théorème de séparation et la décidabilité dans PSPACE de l'appartenance à FO d'un langage reconnu par un automate de Büchi.
 + ** Pour la partie sur les simulations, on pourra consulter le chapitre 7 du livre de Baier et Katoen.
 +-->
 +*/
 +====== Exams ======
 +
 +
 +There will be 2 written exams (E1 and E2) and 2 home assignments (H1 and H2).\\
 +The final mark will be (H1+2E1+H2+2E2)/6.
 +
 +The examination questions will be in French and/or in English depending on the requests.\\
 +Students may write their answers in French or in English.
 +
 +| **Date** | **Type** | **Topics and comments** |
 +|**2012/10/24** | H1: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/homework01.pdf|Alternation-Free Mu-Calculus]] | To hand in on November 7th.\\ Don't be late. |
 +|**2012/11/28** | E1:  | Exam on the first half of the course. |
 +|**2013/01/30** | H2: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/homework02.pdf|Fairness and Petri Nets]] | To hand in on February <del>13th</del>17th.\\ Some [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2012_verif/homework02_answers.pdf|sketches of answers]]. |
 +|**2013/03/06** | E2: [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/exam.pdf|Exam questions]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1213/solution.pdf|sample solutions]] | Exam on the second half of the course. |
 +
 +/*
 +[[http://www.lsv.ens-cachan.fr/~gastin/Verif/Partiel-30-11-11.pdf|Exam]]
 +
 +| **Date** | **Type** | **Topics and comments** |
 +|**2011/10/12** | H1: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/homework01.pdf|Temporal Logic with Binding]] | To hand in on November 2nd.\\ Don't be late. |
 +|**2011/10/12** | H2: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2011_verif/homework02.pdf|Simulations in Petri nets]] | To hand in on February 15th.\\ Don't be late. |
 +|**2012/02/29** | E2: [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/exam.pdf|Exam]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1112/solution.pdf|sample solutions]] | Exam on the second half of the course. |
 +*/
 +
 +/*
 +| **Date** | **Type** | **Topics and comments** |
 +| **2010/10/19** | H1: choose between [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2010_verif/homework01a.pdf|subject H1a (Multi-focus games for LTL)]] and [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2010_verif/homework01b.pdf|subject H1b (A shared key protocol)]] | Treat one subject.  To hand in on November 2nd. |
 +| **2010/11/23** | E1: from 16:15 to 19:15. Chevaleret, **Room 7D01**. [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Partiel-23_11_10.pdf|Subject]]The only authorized documents are the [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1_10_4up.pdf|lecture notes]]|All topics covered during the first half of the semester|
 +| **2011/02/01** | H2: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2010_verif/homework02.pdf|Model checking BPPs]]| To hand in on February 22nd. |
 +| **2011/03/08** | E2: from 16:15 to 18:45.The only authorized documents are the lecture notes (of the entire course).[[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1011/exam.pdf|Exam]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1011/solution.pdf|sample solutions]].|All topics covered during the course, especially the second half.|
 +*/
 +====== Prerequisites ======
 +
 +
 +Finite Automata.
 +
 +====== Related courses ======
 +
 +  * 1-2: Automates avancés et applications
 +  * 1-18: Automates d'arbres et applications
 +  * 2-8: Fondements pour la vérification des systèmes temps-réel
 +  * 2-9: Vérification de systèmes dynamiques et paramétrés
 +  * 2-16: Modélisation par automates finis
 +  * 2-20-1: Jeux pour la théorie des automates, la vérification et l'internet.
 +
 +====== Bibliography ======
 +
 +
 +  * Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.
 +  * Systems and Software Verification. Model-Checking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen. Springer, 2001. \\ Also available in french: Vérification de logiciels : Techniques et outils du model checking. Coordonné par Ph. Schnoebelen. Vuibert, 1999.
 +  * Model Checking. E.M. Clarke, O. Grumberg, D. Peled. MIT Press, 1999.
 +  * Temporal Verification of Reactive Systems - Safety. Zohar Manna and Amir Pnueli. Springer-Verlag, 1995.
 +  * The Temporal Logic of Reactive and Concurrent Systems - Specification. Zohar Manna and Amir Pnueli. Springer-Verlag, 1992.
 +
 +
 +====== Teachers ======
 +
 +
 +|Paul Gastin|PU|ENS Cachan|LSV|
 +|Sylvain Schmitz|MC|ENS Cachan|LSV|
 +|Stefan Schwoon|MC|ENS Cachan|LSV|
 +
 +
 +====== Previous Years ======
 +
 +   * [[2011-2012-c-1-22|2011-2012]]
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA