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/11/08 14:30]
gastin [Motivations and main objectives]
cours:c-1-22 [2019/11/29 09:13] (current)
schwoon [Motivations and main objectives]
Line 66: Line 66:
 | 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]]  | | 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]]  |
 | 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]]  | | 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/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/15 | Büchi emptiness check | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/dfs.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/22 | Partial-order reduction | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/por.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/29 | Binary decision diagrams | [[http://www.lsv.fr/~schwoon/enseignement/verification/ws1819/bdd.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]] | | 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]] |
 | 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]] | | 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]] |
 
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