Bandeau du Laboratoire d'Informatique & Systèmes (LIS)

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

Benjamin MONMEGE

Membres

BAUDRU Nicolas Enseignant/Chercheur
M. BAUDRU Nicolas
Enseignant/Chercheur
nicolas.baudru@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 530
BENALIOUA yahia idriss Doctorant
M. BENALIOUA yahia idriss
Doctorant
yahia-idriss.benalioua@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL
BERTOLISSI Clara Enseignant/Chercheur
Mme BERTOLISSI Clara
Enseignant/Chercheur
clara.bertolissi@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 510
FRATANI Severine Enseignant/Chercheur
Mme FRATANI Severine
Enseignant/Chercheur
severine.fratani@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 521
LEHTINEN Karoliina Chercheur
Mme LEHTINEN Karoliina
Chercheur
karoliina.lehtinen@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 510
LHOTE Nathan Enseignant/Chercheur
M. LHOTE Nathan
Enseignant/Chercheur
nathan.lhote@lis-lab.fr
http://pageperso.lif.univ-mrs.fr/~nathan.lhote/
Luminy, AMU TPR2 ET GRAND HALL, bureau 510
MARTINEZ ANTON Alba Doctorant
M. MARTINEZ ANTON Alba
Doctorant
alba.martinez-anton@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 524
MAURRAS Guillaume Doctorant
M. MAURRAS Guillaume
Doctorant
guillaume.maurras@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL
MONMEGE Benjamin Enseignant/Chercheur
M. MONMEGE Benjamin
Enseignant/Chercheur
benjamin.monmege@lis-lab.fr
https://pageperso.lis-lab.fr/~benjamin.monmege/
Luminy, AMU TPR2 ET GRAND HALL, étage 5, bureau 05.38
MORIN Remi Enseignant/Chercheur
M. MORIN Remi
Enseignant/Chercheur
remi.morin@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 533
OHLMANN Pierre Chercheur
REYNIER Pierre-Alain Enseignant/Chercheur
M. REYNIER Pierre-Alain
Enseignant/Chercheur
pierre-alain.reynier@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 538
TALBOT Jean-Marc Enseignant/Chercheur
M. TALBOT Jean-Marc
Enseignant/Chercheur
jean-marc.talbot@lis-lab.fr
Luminy, AMU TPR2 ET GRAND HALL, bureau 521

Objectif scientifique

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.

Site web de l’équipe

Publications de l’équipe

voir les publications