Lecture notes
-
Course "
Mathematical foundations of the theory of infinite transition systems
" in Master Parisien de Recherche en Informatique (MPRI) -- 2016/2017
-
Slides
for the class on 30/09/2016 (Introduction to Presburger arithmetic, quantifier elimination,
decidability, automata-based approach).
Solution for Exercise 1 (3) can be found in Section 3 of the article
[TCS06]
- Lecture notes "Rudiments of Presburger Arithmetic"
-
Slides
for the class on 07/10/2016 (Semilinear sets, Parikh image of regular languages, introduction to reversal-bounded counter machines).
- Lecture notes "Reversal-bounded counter machines"
-
Course "
Mathematical foundations of the theory of infinite transition systems
" in Master Parisien de Recherche en Informatique (MPRI) -- 2015/2016
-
Slides
for the class on 09/10/2015 (Introduction to Presburger arithmetic, quantifier elimination,
decidability, automata-based approach).
- Lecture notes "Rudiments of Presburger Arithmetic"
- Slides
for the class on 16/10/2015: Semilinear sets, Parikh image of regular languages, Introduction
to reversal-bounded counter machines.
- Slides for the
class on 06/11/2015: Reversal-bounded counter machines: reachability sets, repeated reachability
problems, decidable and undecidable extensions.
- Lecture notes "Reversal-bounded counter machines"
-
Lecture notes "Logical investigations
on separation logics", ESSLLI'15
-
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)
-
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.