![[français]](http://www.lif.univ-mrs.fr/assets/img/lang/fr.png)
Professor, Aix-Marseille University
Teaching at the Computer Science department
of the Faculty of Science
Researcher at
LIS, member of the MoVe team
Co-head (with Jérémie Chalopin) of the Pôle Calcul division of the LIS
Co-head (with Nathalie Bertrand) of the
working group on
Verification of the GDR IM of the 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 : 05.38, TPR2 building
Phone : +33 (0)4 86 09 06 73
Fax : +33 (0)4 86 09 ?? ??
E-mail : firstname.lastname@lis-lab.fr
Research Topics
Formal Methods, Verification, Model-Checking, Automata, Logic,
Transducers, Timed systems, Petri nets, Concurrency, Robustness.
Research Projects (passed/active)
- ANR TickTac: Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems
- ANR DELTA: Challenges for Logic, Transducers and Automata
- PEPS INS2I SOSI: Security of Timed Systems
- 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: Analysis and Conception of Systems with 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
- FP7 QUASIMODO: Quantitative System Properties in Model-Driven-Design of Embedded Systems
Software
Internships
- Master thesis: Quantitative aspects of the robustness of timed automata : Rémy Jaubert (2009)
- L3 (ENS Cachan) Equivalence of Morphims on Context-free Grammars : Rémi Cheval (2010) (co-supervised with Jean-Marc Talbot)
- Master thesis: Bounded Ambiguity of Visibly Pushdown Automata : Mathieu Caralp (2011) (co-supervised with Jean-Marc Talbot)
- L3 (ENS Cachan) Regularity of Visibly Pushdown Transducers: Rémy Poulain (2013)
- Master thesis: Timed Games: Cost and Robustness: Damien Busatto-Gaston (2016) (co-supervised with Benjamin Monmege)
- M1 (ENS Rennes) : Optimal stochastic strategies in weighted games, Julie Parreaux (2019) (with B. Monmege)
- L3 AMU: developing a verification tool, Thomas Galland (2019) (with MoVe colleagues)
- Master thesis: Stochastic strategies in weighted (timed) games, Julie Parreaux (2020) (with B. Monmege)
- L3 ECM: Functionality and sequentiality of transducers, Gabriel Aillet (2020)
PhD Students
- Rémy Jaubert : Implementability and Robustness of Timed Automata (2009-2012), now software engineer
- Mathieu Caralp : Visibly Pushdown Transducers (2011-2015) (co-supervised with Jean-Marc Talbot), now software engineer at Led's chat
- Didier Villevalois : Efficient Evaluation of String Transducers (2015-2019), now software engineer at Volta Medical
- Damien Busatto-Gaston: Weighted Timed Games (2016-2019) (co-supervised with Benjamin Monmege), now post-doc at ULB with Jean-François Raskin
- Léo Exibard: Automatic synthesis of systems with data (2017-2021) (co-supervised with Emmanuel Filiot), now post-doc at Reykjavik University with Antonis Achilleos
- Julie Parreaux: Weighted timed games: randomization and robustness (2020--) (co-supervised with Benjamin Monmege)
- Guillaume Maurras: Logical characterization of higher-order languages (2020--) (co-supervised with Séverine Fratani)
Post-doctoral Students
- Youssouf Oualhadj: Synthesis of robust controllers, 2012-2013, now assistant professor at Paris-Est Créteil
- Laure Daviaud: Cost functions for nested words, 2014-2015, now Lecturer at City University, London
- Luc Dartois: First-order definable regular string functions, 2014-2015, now assistant professor at Paris-Est Créteil
- Antoine Durand-Gasselin: Transductions of data-words, 2015-2016
- Louis-Marie Dando : Weighted automata and expressions, 2020-2021, now post-doc at IMDEA, Madrid