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:2015-2016-c-1-22 [2016/09/15 11:30]
schmitz created
cours:2015-2016-c-1-22 [2016/09/15 16:15] (current)
schmitz
Line 1: Line 1:
-Hello world!+ 
 +====== Basics of Verification (60h, 6 ECTS) ====== 
 + 
 + 
 +In charge: [[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]] (LSV, ENS Cachan). 
 + 
 +====== Lecturers in 2015—2016====== 
 + 
 +[[http://www.lsv.ens-cachan.fr/~chatain/|Thomas Chatain]],  
 +[[http://www.lsv.ens-cachan.fr/~schmitz/|Sylvain Schmitz]], 
 +[[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]],  
 +[[http://www.lsv.ens-cachan.fr/~dstan/|Daniel Stan]]. 
 + 
 + 
 +/*====== Research internships ====== 
 + 
 +  * [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Verification of concurrent systems with data structures]] 
 +  * [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Probabilistic specifications]] 
 +  * [[http://www.lsv.ens-cachan.fr/~gastin/Verif/index.php|Synthesis of Distributed Systems with Parameterized Network Topology]] 
 + 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 ====== 
 + 
 +Here are some [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2015_verif/notes.pdf|rough notes]] covering most of the first half. 
 + 
 +Here are the planned contents for the first half of the course (which might change slightly): 
 + 
 +^ Date ^ Topics covered ^ 
 +| 2015/09/15 | **Introduction** & motivation [[http://www.lsv.ens-cachan.fr/~chatain/enseignement/verif/intro_verif.pdf|slides]] \\ **Finite-state models**: transition systems\\ **Temporal frames**: modal logic, first-order logic| 
 +| 2015/09/22 | **Branching time**: CTL model-checking\\ CTL<sup>*</sup>, fair CTL, CTL<sup>+</sup>| 
 +| 2015/09/29 | **Linear time**: LTL\\ **Büchi automata** (BA)| 
 +| 2015/10/06 | **very weak alternating Büchi automata** (vwABA)\\ translation from LTL to vwABA to BA| 
 +| 2015/10/13 | **Upper bounds**: PSPACE-easiness of LTL and CTL<sup>*</sup> model-checking| 
 +| 2015/10/20 | **Lower bounds**: PSPACE-hardness of LTL and CTL<sup>*</sup> model-checking| 
 +| 2015/11/03 | **High-level models**\\ SPIN| 
 +| 2015/11/24 | Lecture ([[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/dfs.pdf|Depth-First Search]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/por.pdf|Partial-Order Reduction]]) | 
 +| 2015/12/01 | Lecture (Partial-Order Reduction, [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/bdd.pdf|Binary Decision Diagrams]]) | 
 +| 2015/12/08 | Lecture (Binary Decision Diagrams, [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/refine.pdf|Abstraction/Refinement]]) | 
 +| 2015/12/15 | Lecture (Abstraction/Refinement, [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/bmc.pdf|Bounded Model-Checking]]) | 
 +| 2016/01/05 | Lecture (Petri nets, [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1516/nets.pdf|preliminary slides]]) | 
 + 
 +/* 
 +| **2013/09/25** | [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif13/td01.pdf|Exercises]] | Mutual exclusion algorithms, Handshake with data exchange, Needham-Schroeder protocol, Channel systems| 
 +| **2013/10/09** | [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif13/td02.pdf|Exercises]] | Temporal Logics: LTL, CTL<sup>*</sup>, CTL, CTL<sup>+</sup>| 
 +| **2013/10/16** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-13-lecture3-4up.pdf|Lecture]] | CTL, PTIME model checking algorithm for CTL and for fair-CTL \\ Büchi automata | 
 +| **2013/10/23** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/td03.pdf|Exercises]] | CTL model checking and Büchi automata | 
 +| **2013/10/30** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-13-lecture4-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> \\  | 
 +| **2013/11/06** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/td04.pdf|Exercises]] | LTL model checking and complexity | 
 +| **2013/11/13** | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-13-lecture5-4up.pdf|Lecture]] | Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation | 
 +| **2013/11/20** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/td05.pdf|Exercises]] | EF Games, Separation | 
 +| **2013/12/11** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/bdd.pdf|Lecture]] | Binary Decision Diagrams | 
 +| **2013/12/18** | [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif13/td06.pdf|Exercises]] | BBDs | 
 +| **2014/01/08** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/nets.pdf|Lecture]] | Petri Nets | 
 +| **2014/01/15** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/td07.pdf|Exercises]] | Petri nets, Coverability | 
 +| **2014/01/22** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/nets.pdf|Lecture]] | Petri Nets | 
 +| **2014/01/28** | [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/td08.pdf|Exercises]] | Unfoldings, Vector Addition Systems | 
 +| **2014/02/05** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/por.pdf|Lecture]] | Partial-Order Reduction | 
 +| **2014/02/12** | [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif13/td09.pdf|Exercises]] | Partial-Order Reduction | 
 +| **2014/02/19** | [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/refine.pdf|Lecture]] | Abstraction and Refinement | 
 +*/ 
 + 
 +====== 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 ^ 
 +|**2015/09/29** | H1: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2015_verif/homework01.pdf|First-order logic with 2 variables]]  | To hand in on October 13th.\\ Don't be late.| 
 +|**2015/12/17** | H2: [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif15/homework2.pdf|Symmetric Model Checking]]  | To hand in on January 5th 2015.| 
 +|**2016/01/12** | E2: final exam | Exam on the second half of the course, room C509, 9h-11h | 
 + 
 +/* [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1415/exam.pdf|final exam]], [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1415/solution.pdf|solutions]]  */ 
 +/* |**2013/10/30** | H1: [[http://www.lsv.ens-cachan.fr/~dstan/teaching/verif13/homework01.pdf|Dynamic Logics]] | To hand in on November 13th.\\ Don't be late. | */ 
 +/* |**2014/01/28** | H2: [[http://www.lsv.ens-cachan.fr/~schmitz/teach/2013_verif/homework02.pdf|Petri Nets Coverability]]| To hand in on February 12th.\\ Don't be late. | */ 
 + 
 + 
 +/*======= Exams from previous years ======= 
 +Concerning the second part of the course, the exams and solutions of previous years can be found in the pages for previous editions of the course (see the links at the bottom of the page), except for 2013-14, which are [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/exam.pdf|here]] (exam) and [[http://www.lsv.ens-cachan.fr/~schwoon/enseignement/verification/ws1314/solution.pdf|here]] (solutions). */ 
 + 
 +====== Prerequisites ====== 
 + 
 + 
 +Finite Automata\\ 
 +First-order logic 
 + 
 +====== Related courses ====== 
 + 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-1-18|1-18: Tree automata and applications]] 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-8-1|2-8-1: Non-sequential theory of distributed systems]] 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-8-2|2-8-2: Foundations of real time and hybrid systems]] 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-9-1|2-9-1: Mathematical foundations of the theory of infinite transition systems]] 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-9-2|2-9-2: Algorithmic verification of programs]] 
 +  * [[https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-20-1|2-20-1: Game theoretic techniques in computer science]] 
 + 
 +====== 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 ====== 
 + 
 + 
 +|Sylvain Schmitz|MC|ENS Cachan|LSV| 
 +|Thomas Chatain|MC|ENS Cachan|LSV| 
 +|Stefan Schwoon|MC|ENS Cachan|LSV| 
 +|Daniel Stan|PhD|ENS Cachan|LSV| 
 + 
 + 
 +====== Previous Years ====== 
 + 
 +   * [[2014-2015-c-1-22|2014-2015]] 
 +   * [[2013-2014-c-1-22|2013-2014]] 
 +   * [[2012-2013-c-1-22|2012-2013]] 
 +   * [[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