Pierre-Alain Reynier

Professeur, Université d'Aix-Marseille, Département Informatique et Interactions

Chercheur au LIS

Responsable de l'équipe Modélisation et Vérification (MoVe) du LIS

Responsable du Parcours Informatique et Mathématiques Discrètes du Master Informatique.

Co-responsable (avec Nathalie Bertrand) du groupe de travail Vérification du GDR-IM du CNRS

Contact :

Laboratoire d’Informatique et Systèmes
Parc Scientifique de Luminy
163 avenue de Luminy - Case 901
F-13288 Marseille Cedex 9, France

Office : A208 (bibilothèque universitaire, 2ème étage)
Phone : +33 (0)4 86 09 06 73
Fax : +33 (0)4 86 09 ?? ??

E-mail : prénom.nom@lis-lab.fr (Nouveau !)

Thèmes de recherche

Formal Methods, Verification, Model-Checking, (Timed) Automata, (Timed) Petri nets, Concurrency, Robustness, Temporal logics.

Projets de recherche (en cours/passés)

ANR DELTA: Défis pour la logique, les transducteurs et les automates
PEPS INS2I SOSI: Sécurité des systèmes temporisés
PHC Tournesol VAST: Verification And Synthesis of Transformations
PEPS INS2I SOSP: Synthesis of Stream Processors
ANR MACARON: Moving and Computing: Agents, Robots and Networks
FP7 Cassting: Collective Adaptative Systems Synthesis With Non-zero-sum Games
ANR ImpRo: Implementability and Robustness of Timed Systems
ANR JCJC ECSPER: Etude et Conception de Systèmes avec Perturbations
ACI SI CORTOS: Control and Observation of Real-Time Open Systems
ANR DOTS: Distributed, Open and Timed Systems
PAI MoVES: Modelling, Verification and Evolution of Software
QUASIMODO: Quantitative System Properties in Model-Driven-Design of Embedded Systems

Logiciels

Nouveau ! Outil développé avec Florent Jaillet en C++ calculant l'ensemble minimal de couverture d'un réseau de Petri.
Prototype en Python implémentant notre algorithme calculant l'ensemble minimal de couverture d'un réseau de Petri.
Prototype fondé sur l'outil UppAal pour le traitement des gardes diagonales dans les automates temporisés.

Stages

M2 Recherche Aspects quantitatifs de la robustesse des automates temporisés : Rémy Jaubert (2009)
L3 (ENS Cachan) Equivalence de morphismes sur des grammaires hors-contexte : Rémi Cheval (2010) (co-encadré avec Jean-Marc Talbot)
M2 Recherche Ambiguité bornée des automates a pile visible : Mathieu Caralp (2011) (co-encadré avec Jean-Marc Talbot)
L3 (ENS Cachan) Regularity of Visibly Pushdown Transducers: Rémy Poulain (2013)
M2 Recherche: Timed Games: Cost and Robustness: Damien Busatto-Gaston (2016) (co-encadré avec Benjamin Monmege)

Doctorants

Rémy Jaubert : Implementability and Robustness of Timed Automata (2009-2012), ingénieur
Mathieu Caralp : Visibly Pushdown Transducers (2011-2015) (co-encadré avec Jean-Marc Talbot), ingénieur chez Led's chat
Didier Villevalois: Efficient Evaluation of String Transducers (2015--)
Damien Busatto-Gaston: Weighted Timed Games (2016--) (co-encadré avec Benjamin Monmege)
Léo Exibard: Automatic synthesis of systems with data (2017--) (co-encadré avec Emmanuel Filiot)

Post-doctorants

Youssouf Oualhadj: Synthesis of robust controllers, 2012-2013, mâitre de conférences à Paris-Est Créteil
Laure Daviaud: Cost functions for nested words, 2014-2015, post-doc à l'Université de Warwick
Luc Dartois: First-order definable regular string functions, 2014-2015, post-doc à l'ULB
Antoine Durand-Gasselin: Transductions of data-words, 2015-2016