Lecture notes

Course " Verification of parametrized and dynamic systems " in Master Parisien de Recherche en Informatique (MPRI)
- Slides for the class on 10/12/2010 (VASS, VAS, coverability graphs, Rackoff's proof for the EXPSPACE upper bound of the covering problem, weak multiplication, etc.).
- Slides for the class on 17/12/2010 (EXPSPACE-hardness proof for reachability problems for VASS, introduction to reversal-bounded counter automata).
- Slides for the class on 07/01/2011 (semilinearity of reversal-bounded counter automata).
- Slides for the class on 14/01/2011 (reachability problems for reversal-bounded CA, affine counter systems with finite monoid property).
- Slides for the class on 21/01/2011 (LTL for admissible counter systems and exercises).
Counter systems and temporal logics (U. of Buenos Aires and U. Nacional de Córdoba, October/November 2010)
Decidable problems for counter systems (ESSLLI'10 advanced course, August 2010)
Cours " Fondements pour la vérification des systèmes temps-réel et concurrents " du Master Parisien de Recherche en Informatique (MPRI)
- Transparents du cours du 24/09/07.
- Transparents du cours du 01/10/07.
- Transparents du cours du 08/10/07.
Temporal logics and verification of infinite-state systems (ESSLLI'07 advanced course)
S. Demri. Temporal logics . MPRI, 2005/2006.
S. Demri. Logiques modales et méthode des tableaux: une introduction . MPRI, 2004/2005. Transparents, 86 pages.
S. Demri. Complexité algorithmique de variantes des LTL pour la vérification . DEA Algorithmique, 2003/2004. 90 pages.
S. Demri. Algorithmique: problème du flot maximal, NP-complétude et algorithmes d'approximation . Magistère STIC, ENS Cachan, 2002/2003. 50 pages.
S. Demri. Logique et Formalisation du Raisonnement: Part II - Logiques Non classiques . DEA Informatique, Systèmes et Communications (ENSIMAG, Université Joseph Fourier, Grenoble), 1998/1999. 27 pages.