MOVE : Modélisation et Vérification

Mots clés

Vérification : Model-Checking, Synthèse, Robustesse ; Automates et leurs extensions : Transducteurs, Ordre supérieur, Automates quantitatifs, Automates probabilistes, Automates temporisés, Systèmes d’addition de vecteurs ; Logique : Logique monadique, Logiques temporelles ; Sécurité : Réécriture, Contrôle d’accès, Calculs de processus.

 

Responsable

Pierre-Alain REYNIER

 

Membres permanents

BAUDRU NicolasMaitre de Conférences
Courriel : nicolas.baudru@lis-lab.fr
Telephone : 0486090454
Page personnelle : https://pageperso.lis-lab.fr/nicolas.baudru/
BERTOLISSI ClaraMaitre de Conférences
Courriel : clara.bertolissi@lis-lab.fr
Telephone : 0486090456
Page personnelle : https://pageperso.lis-lab.fr/clara.bertolissi/
FRATANI SéverineMaitre de Conférences
Courriel : severine.fratani@lis-lab.fr
Telephone : 0486090468
Page personnelle : https://pageperso.lis-lab.fr/severine.fratani/
LUGIEZ DenisProfesseur des Universités
Courriel : denis.lugiez@lis-lab.fr
Telephone : 0486090487
Page personnelle : https://pageperso.lis-lab.fr/denis.lugiez/
MONMEGE BenjaminMaitre de Conférences
Courriel : benjamin.monmege@lis-lab.fr
Telephone : 0486090489
Page personnelle : https://pageperso.lis-lab.fr/benjamin.monmege/
MORIN RémiProfesseur des Universités
Courriel : remi.morin@lis-lab.fr
Telephone : 0486090490
Page personnelle : https://pageperso.lis-lab.fr/remi.morin/
REYNIER Pierre-AlainMaitre de Conférences
Courriel : pierre-alain.reynier@lis-lab.fr
Telephone : 0486090673
Page personnelle : https://pageperso.lis-lab.fr/pierre-alain.reynier/
TALBOT Jean-MarcProfesseur des Universités
Courriel : jean-marc.talbot@lis-lab.fr
Telephone : 0486090681
Page personnelle : https://pageperso.lis-lab.fr/jean-marc.talbot/

 

Doctorants

BUSATTO DamienDoctorant
Courriel : damien.busatto@lis-lab.fr
Telephone : 0486090484
Page personnelle : https://pageperso.lis-lab.fr/damien.busatto/
EXIBARD LéoDoctorant
Courriel : leo.exibard@lis-lab.fr
LOPEZ TheodoreDoctorant
Courriel : theodore.lopez@lis-lab.fr
VILLEVALOIS DidierDoctorant
Courriel : didier.villevalois@lis-lab.fr
Telephone : 0486090484
Page personnelle : https://pageperso.lis-lab.fr/didier.villevalois/
VOUNDY MakkiDoctorant
Courriel : makki.voundy@lis-lab.fr
Page personnelle : https://pageperso.lis-lab.fr/makki.voundy/

 

Autres membres

 

Objectif scientifique

L’équipe MOVE (Modélisation et Vérification), localisée sur le campus de Luminy, s’intéresse au développement de techniques de vérification formelle pour les systèmes logiciels. Plus précisément, l’équipe travaille sur les fondements théoriques de ces outils, et en particulier les approches fondées sur les automates et la logique, comme le model-checking et la synthèse. Ces travaux consistent à étudier différentes extensions de ces modèles sous les perspectives de l’expressivité, de la décidabilité et de questions algorithmiques. Par ailleurs, l’équipe travaille également à l’utilisation de méthodes formelles dans le domaine de la sécurité des systèmes informatiques en utilisant des outils comme la réécriture et les calculs de processus.Le projet scientifique de l’équipe est ainsi organisé selon trois axes :

  1. Langages et transformations : cet axe regroupe les activités en lien avec l’étude des modèles sous-jacents aux techniques de vérification.
  2. Techniques symboliques pour la vérification : cet axe correspond aux travaux algorithmiques en lien principalement avec les problèmes de model-checking et de synthèse.
  3. Sécurité : cet axe regroupe les travaux concernant le développement et l’utilisation de méthodes formelles pour des questions de sécurité, comme le contrôle d’accès ou la vérification de propriétés de protocoles cryptographiques.

 

Publications récentes de l’équipe



14 documents

Article dans une revue

  • Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier, Frédéric Servais. Streamability of nested word transductions. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019. ⟨hal-02103898⟩
  • Serge Haddad, Benjamin Monmege. Interval Iteration Algorithm for MDPs and IMDPs. Theoretical Computer Science, Elsevier, 2018, 735, pp.111 - 131. ⟨10.1016/j.tcs.2016.12.003⟩. ⟨hal-01809094⟩
  • Luc Dartois, Ismaël Jecker, Pierre-Alain Reynier. Aperiodic String Transducers. International Journal of Foundations of Computer Science, World Scientific Publishing, 2018. ⟨hal-02003676⟩
  • Paul Gastin, Benjamin Monmege. A Unifying Survey on Weighted Logics and Weighted Automata: Core Weighted Logic: Minimal and Versatile Specification of Quantitative Properties. Soft Computing, Springer Verlag, 2018, 22 (4), pp.1047-1065. ⟨10.1007/s00500-015-1952-6⟩. ⟨hal-01130216v2⟩
  • Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier, Jean-Marc Talbot. Decision problems of tree transducers with origin. Information and Computation, Elsevier, 2018, 261, pp.311-335. ⟨10.1016/j.ic.2018.02.011⟩. ⟨hal-02093317⟩
  • Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier, Frédéric Servais, Jean-Marc Talbot. Visibly pushdown transducers. Journal of Computer and System Sciences, Elsevier, 2018, 97, pp.147-181. ⟨10.1016/j.jcss.2018.05.002⟩. ⟨hal-02093318⟩

Communication dans un congrès

  • Théodore Lopez, Benjamin Monmege, Jean-Marc Talbot. Determinisation of Finitely-Ambiguous Copyless Cost Register Automata. 44th International Symposium on Mathematical Foundations of Computer Science, Aug 2019, Aachen, Germany. ⟨10.4230/LIPIcs.MFCS.2019.75⟩. ⟨hal-02268107⟩
  • Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier, Ocan Sankur. Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach. 31st International Conference on Computer Aided Verification, Jul 2019, New-York, United States. pp.572-590. ⟨hal-02264083⟩
  • Thomas Brihaye, Arthur Milchior, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege. Efficient algorithms and tools for MITL model-checking and synthesis. 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), Dec 2018, Melbourne, Australia. ⟨hal-02014073⟩
  • Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), Dec 2018, Ahmedabad, India. ⟨10.4230/LIPIcs.FSTTCS.2018.28⟩. ⟨hal-02014051⟩
  • Nicolas Baudru, Pierre-Alain Reynier. From Two-Way Transducers to Regular Function Expressions. 22nd International Conference on Developments in Language Theory (DLT 2018), Sep 2018, Tokyo, Japan. pp.96-108, ⟨10.1007/978-3-319-98654-8_8⟩. ⟨hal-02003430⟩
  • Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, et al.. Optimal and Robust Controller Synthesis: Using Energy Timed Automata with Uncertainty. FM 2018 - International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.203-221, ⟨10.1007/978-3-319-95582-7_12⟩. ⟨hal-01889222⟩
  • Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or. Automata, Languages and Programming, 33rd International Colloquium, , Jul 2006, Venise, Italy. ⟨hal-01759947⟩

Direction d'ouvrage, Proceedings