Launching LMF - the Formal Methods Laboratory

The Laboratoire Méthodes Formelles (LMF) was founded on 1 January 2021 as a joint research centre of University Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, and CentraleSupélec with a main focus on formal methods. The new laboratory combines the expertise of about 100 members from the former Laboratoire Spécification et Vérification (LSV) and the VALS team of Laboratoire de Recherche en Informatique (LRI).

In our mission to enlighten the digital world through Mathematical Logic, we rely on formal methods as a tool to analyse, model, and reason about computing systems, such as computer programs, security protocols, and hardware designs. Our research targets a wide range of computational paradigms, from classical to emerging ones such as biological and quantum computing.

LMF is structured around three hubs: Proofs and Models, which lie at the heart of our historical background, and Interactions, that is aimed at fostering cross-fertilisation between formal methods and other domains in computing science and beyond.

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 : Safouan Taha, Burkhart Wolff
  • Parité-égalité : Caroline Fontaine
  • Valorisation : Jacques-Henri Jourdan
  • Europe : Matthias Függer
  • Développement durable : Thomas Chatain
  • HAL : Frédéric Boulanger
  • Cellule doctorants et doctorantes : Sylvie Boldo (permanence régulièrement le jeudi de 13h à 14h au 650, bureau 62), Benedikt Bollig (permanence régulièrement le jeudi de 13h à 14h à l'ÉNS, bureau 2S60), Chantal Keller (permanence régulièrement le jeudi (hors vacances scolaires) de 13h à 14h à l'ÉNS, bureau 2S61), Stéphane Le Roux (présence régulière à l'ÉNS, bureau 2S56)
  • Allocation des bureaux : Dietmar Berwanger, Safouan Taha

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.