Création du Laboratoire Méthodes Formelles

Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV, ENS Paris-Saclay, CNRS, Inria) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI, Université Paris-Saclay, CNRS, Inria, CentraleSupélec) soit une centaine de personnes.

Son ambition est d’éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d’analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l’informatique quantique.

Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles » ; le troisième, « Interactions », est une ouverture à d’autres domaines tels que l’IA et la biologie.

Les tutelles du laboratoire

Le Laboratoire Méthodes Formelles est une unité mixte de recherche (UMR 9021) de l'Université Paris-Saclay, du CNRS et de l'ENS Paris-Saclay. Il a également deux tutelles secondaires, CentraleSupélec et Inria.

Organisation

L'organigramme fonctionnel simplifié du laboratoire est disponible ci-dessous :

Le laboratoire a en outre plusieurs référents ou correspondants :

  • Formations (CoFo) : Marie-France Grandisson
  • Communication : Dietmar Berwanger
  • Web : Dietmar Berwanger, Frédéric Boulanger
  • Séminaires : Burkhart Wolff
  • Parité-égalité : Caroline Fontaine
  • Valorisation : Jacques-Henri Jourdan
  • Plateformes : Jean-Christophe Filliâtre
  • Europe : Matthias Függer
  • Développement durable : Thomas Chatain
  • HAL : Frédéric Boulanger
  • Cellule doctorants et doctorantes : Sylvie Boldo, Benedikt Bollig, Chantal.Keller, Stéphane Le Roux
  • Représentants des doctorants : Fabricio Cravo, Louis Lemonnier
  • Chargé de mission pour les infrastructures : Dietmar Berwanger, en liaison avec le service informatique
  • Allocation des bureaux : Dietmar Berwanger, Frédéric Voisin

Venir au LMF

Le laboratoire est localisé à Gif-sur-Yvette sur le plateau de Saclay.

Par les transports en commun

  • RER B ( Saint-Rémy-lès-Chevreuse) ou RER C ( Massy-Palaiseau) -- Arrêt : « Massy-Palaiseau »
    • Puis prendre un des bus suivants :
      • Bus 91.06C (Christ de Saclay)
      • Bus 91.06B (Saint-Quentin-en-Yvelines)
      • Bus 91.10 (Saclay)
    • Arrêt : « Moulon » (20 minutes depuis la gare).
  • RER B ( Saint-Rémy-lès-Chevreuse) -- Arrêt : « Le Guichet »
    • Puis prendre le bus suivant :
      • Bus 9 (Christ de Saclay)
    • Arrêt : « Moulon » (5/10 minutes depuis la gare).
  • Bus 91.08 (Polytechnique Vauve / Fresnel) -- Arrêt « Université Paris-Saclay ».

En voiture

  • Par la N118 : Pont de Sèvres, suivre « Nantes-Bordeaux ». Sortie 9 : « Centre Universitaire ». Au rond-point prendre la deuxième sortie.
  • Par l’A6 : Prendre A6 puis l'A10 direction « Nantes-Bordeaux ». Suivre la direction « Cité Scientifique » puis « Saclay ». Poursuivre sur la D36. Tourner à gauche sur D128 direction « Centre Universitaire ». Passer 2 ronds-points. Au 3e prendre la 2e sortie.