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:c-1-22 [2019/01/16 21:52]
schwoon [Exams]
cours:c-1-22 [2020/01/16 15:09] (current)
schwoon [Exams]
Line 5: Line 5:
 In charge: [[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]] (LSV, ENS Cachan). In charge: [[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]] (LSV, ENS Cachan).
  
-====== Lecturers in 2018—2019======+====== Lecturers in 2019—2020======
  
 [[http://www.lsv.ens-cachan.fr/~gastin/|Paul Gastin]],  [[http://www.lsv.ens-cachan.fr/~gastin/|Paul Gastin]], 
 [[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]], [[http://www.lsv.ens-cachan.fr/~schwoon/|Stefan Schwoon]],
-[[http://www.lsv.ens-cachan.fr/~fortin|Marie Fortin]].+[[http://www.lsv.ens-cachan.fr/~thomasset|Nathan Thomasset]].
  
 /*====== Research internships ====== /*====== Research internships ======
Line 47: Line 47:
  
  ====== Detailed description and Lecture notes ======  ====== Detailed description and Lecture notes ======
 +
 +/*
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw1.pdf|Homework1]] \\ [[http://www.lsv.fr/~fortin/verif2018/td01.pdf|Exercises]]
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw2.pdf|Homework2]] \\ [[http://www.lsv.fr/~fortin/verif2018/td02.pdf|Exercises]]
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw3.pdf|Homework3]] \\ [[http://www.lsv.fr/~fortin/verif2018/td03.pdf|Exercises]]
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw4.pdf|Homework4]] \\ [[http://www.lsv.fr/~fortin/verif2018/td04.pdf|Exercises]]
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw5.pdf|Homework5]] \\ [[http://www.lsv.fr/~fortin/verif2018/td05.pdf|Exercises]]
 +\\ Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation
 +\\ [[http://www.lsv.fr/~fortin/verif2018/hw6.pdf|Homework6]] \\ [[http://www.lsv.fr/~fortin/verif2018/td06.pdf|Exercises]]
 +*/
  
 ^ Date ^ Topics covered ^ Documents ^ ^ Date ^ Topics covered ^ Documents ^
-2018/09/20 | Introduction & motivation \\ **Models**: Transition systems (Kripke structures), variables, synchronized products, Rendez-vous, \\ shared variables, atomicity, asynchronous communication, FIFO channels | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw1.pdf|Homework1]] \\ [[http://www.lsv.fr/~fortin/verif2018/td01.pdf|Exercises]] | +2019/09/20 | Introduction & motivation \\ **Models**: Transition systems (Kripke structures), variables, synchronized products, Rendez-vous, \\ shared variables, atomicity, asynchronous communication, FIFO channels | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]] | 
-2018/09/27 | Specification: introduction, linear vs branching specifications, first-order vs temporal logics \\ Linear temporal logics: definitions, examples, model checking | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw2.pdf|Homework2]] \\ [[http://www.lsv.fr/~fortin/verif2018/td02.pdf|Exercises]] | +2019/09/27 | Specification: introduction, examples, temporal structures, first-order vs temporal logics \\ Linear temporal logics: definitions, examples, model checking | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]] | 
-2018/10/04 | Branching specificationsMSO, CTL<sup>*</sup>, CTL: definitions, examples, model checking | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw3.pdf|Homework3]] \\ [[http://www.lsv.fr/~fortin/verif2018/td03.pdf|Exercises]] +2019/10/04 | linear vs branching specifications, Branching specifications. \\ MSO, CTL<sup>*</sup>, CTL: definitions, examples, model checking | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]] | 
-2018/10/11 | PTIME Model checking algorithm for CTL and for CTL with fairness \\ Büchi automata: definition and first examples | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw4.pdf|Homework4]] \\ [[http://www.lsv.fr/~fortin/verif2018/td04.pdf|Exercises]] +| 2019/10/11 | Cancelled | | 
-2018/10/18 | Büchi automata: main properties, generalized acceptance, unambiguity \\ Sequential Büchi transducers: definition and examples \\ Sequential Büchi transducer for basic LTL formulas \\ Construction of a sequential Büchi transducer for an arbitrary LTL formula | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw5.pdf|Homework5]] \\ [[http://www.lsv.fr/~fortin/verif2018/td05.pdf|Exercises]] +2019/10/18 | PTIME Model checking algorithm for CTL and for CTL with fairness | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]]  
-2018/10/25 | Satisfiability and Model checking for LTL: decidability and complexity \\ PSPACE model checking algorithm for CTL<sup>*</sup> \\ Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-18-handout.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw6.pdf|Homework6]] \\ [[http://www.lsv.fr/~fortin/verif2018/td06.pdf|Exercises]] +2019/10/25 | Büchi automata: definition, examples, main properties, generalized acceptance, unambiguity \\ Sequential Büchi transducers: definition and examples \\ Sequential Büchi transducer for basic LTL formulas | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]]  
-2018/11/15 | Büchi emptiness check | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/dfs.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw7.pdf|Homework7]] \\ [[http://www.lsv.fr/~fortin/verif2018/td07.pdf|Exercises]] | +2019/11/08 Construction of a sequential Büchi transducer for an arbitrary LTL formula \\ Satisfiability and Model checking for LTL: decidability and complexity \\ PSPACE model checking algorithm for CTL<sup>*</sup> | [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Verif-M1-19-handout.pdf|Slides]]  
-2018/11/22 | Partial-order reduction | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/por.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw8.pdf|Homework8]] \\ [[http://www.lsv.fr/~fortin/verif2018/td08.pdf|Exercises]] | +2019/11/15 | Büchi emptiness check | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/dfs.pdf|Slides]] | 
-2018/11/29 | Binary decision diagrams | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/bdd.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw9.pdf|Homework9]] \\ [[http://www.lsv.fr/~fortin/verif2018/td09.pdf|Exercises]] |  +2019/11/22 | Partial-order reduction | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/por.pdf|Slides]] | 
-2018/12/06 | Petri nets | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/nets.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw10.pdf|Homework10]] \\ [[http://www.lsv.fr/~fortin/verif2018/td10.pdf|Exercises]] | +2019/11/29 | Binary decision diagrams | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/bdd.pdf|Slides]] |  
-2018/12/13 | Petri nets | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/nets.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw11.pdf|Homework11]] \\ [[http://www.lsv.fr/~fortin/verif2018/td11.pdf|Exercises]] | +2019/12/06 | Petri nets | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/nets.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw10.pdf|Homework10]] \\ [[http://www.lsv.fr/~fortin/verif2018/td10.pdf|Exercises]] | 
-2018/12/20 | Petri nets, Pushdown systems | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/pds.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw12.pdf|Homework12]] \\ [[http://www.lsv.fr/~fortin/verif2018/td12.pdf|Exercises]] | +2019/12/13 | Petri nets | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/nets.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw11.pdf|Homework11]] \\ [[http://www.lsv.fr/~fortin/verif2018/td11.pdf|Exercises]] | 
-2019/01/10 | Pushdown systems, Abstraction/refinement | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/refine.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2017/hw9.pdf|Homework9]] \\ [[http://www.lsv.fr/~fortin/verif2017/td11.pdf|Exercises]] | +2019/12/20 | Petri nets, Pushdown systems | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/pds.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2018/hw12.pdf|Homework12]] \\ [[http://www.lsv.fr/~fortin/verif2018/td12.pdf|Exercises]] | 
 +2020/01/10 | Abstraction/refinement | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/refine.pdf|Slides]] \\ [[http://www.lsv.fr/~fortin/verif2017/hw9.pdf|Homework9]] \\ [[http://www.lsv.fr/~fortin/verif2017/td11.pdf|Exercises]] | 
    
 ====== Exams ====== ====== Exams ======
Line 67: Line 78:
 This years's mid-term exam: This years's mid-term exam:
  
-Final exam: January 17, 201914h-16h. All course materials can be used.+Final exam: January 17, 202010h-12h. All course materials can be used.
  
 Last years's subjects for mid-term exams: Last years's subjects for mid-term exams:
 +[[http://www.lsv.ens-cachan.fr/~gastin/Verif/Partiel-18.pdf|2018 subject]]
 [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Partiel-17.pdf|2017 subject]] [[http://www.lsv.ens-cachan.fr/~gastin/Verif/Partiel-17.pdf|2017 subject]]
 [[http://www.lsv.fr/~chatain/enseignement/verif/partiel_verif_2016.pdf|2016 subject]], [[http://www.lsv.fr/~chatain/enseignement/verif/partiel_verif_2016.pdf|2016 subject]],
Line 135: Line 147:
 |Paul Gastin|PR|ENS Paris-Saclay|LSV| |Paul Gastin|PR|ENS Paris-Saclay|LSV|
 |Stefan Schwoon|MC|ENS Paris-Saclay|LSV| |Stefan Schwoon|MC|ENS Paris-Saclay|LSV|
-|Marie Fortin|PhD|ENS Paris-Saclay|LSV|+|Nathan Thomasset|PhD|ENS Paris-Saclay|LSV|
  
  
 ====== Previous Years ====== ====== Previous Years ======
  
 +   * [[2018-2019-c-1-22|2018-2019]]
    * [[2017-2018-c-1-22|2017-2018]]    * [[2017-2018-c-1-22|2017-2018]]
    * [[2016-2017-c-1-22|2016-2017]]    * [[2016-2017-c-1-22|2016-2017]]
Line 147: Line 160:
    * [[2012-2013-c-1-22|2012-2013]]    * [[2012-2013-c-1-22|2012-2013]]
    * [[2011-2012-c-1-22|2011-2012]]    * [[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