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/10/04 18:15]
gastin
cours:c-1-22 [2019/10/20 17:45] (current)
gastin [Motivations and main objectives]
Line 52: Line 52:
 \\ [[http://www.lsv.fr/~fortin/verif2018/hw2.pdf|Homework2]] \\ [[http://www.lsv.fr/~fortin/verif2018/td02.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/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]]
 */ */
  
 ^ Date ^ Topics covered ^ Documents ^ ^ Date ^ Topics covered ^ Documents ^
-| 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-18-handout.pdf|Slides]] | +| 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]] | 
-| 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-18-handout.pdf|Slides]] | +| 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]] | 
-| 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-18-handout.pdf|Slides]] | +| 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/18 | 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 \\ 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]] |
 | 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]] | | 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]] |
 | 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]] | | 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]] |
 
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