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.

Partenaires Industriels

  • AVSimulation
  • EDF
  • PSA
  • Quandela
  • Renault
  • SystemX
  • Valeo

Partenaires Academiques

CEA, INRIA, LORIA, LISN lab of Paris-Saclay University, CRIL, IRIF, IRIT - Toulouse, LACL Lab of UPEC University, Max Planck Institute for Software Systems: MPI SWS - Germany, Institute for Software Engineering and Programming Languages - Germany, AnSyMo group of Antwerp University, MDSL Lab of McGill University, Udela - Universidad de la República - Uruguay, UBA - Buenos Aires University.

 

Rapport LMF 2022

A télécharger ICI

Contact

Site web

LMF - Laboratoire Méthodes Formelles
4 avenue des Sciences
91190 Gif-sur-Yvette, France

Téléphone : +33 (0)1 81 87 54 50

Directrice Patricia Bouyer-Decitre
Mail : lmf-contact[at]lsv.fr

Les dernières publications

Communication dans un congrès
01/02/2024
Quantum Circuit Completeness: Extensions and Simplifications
Alexandre Clément, Noé Delorme, Simon Perdrix, Renaud Vilmart
Communication dans un congrès
17/01/2024
The Logical Essence of Well-Bracketed Control Flow
Amin Timany, Armaël Guéneau, Lars Birkedal
Communication dans un congrès
17/01/2024
Thunks and Debits in Separation Logic with Time Credits
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
Article dans une revue
01/01/2024
Article dans une revue
01/01/2024
Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna, Mickaël Laurent, Kim Nguyen
Voir toutes les publications du laboratoire sur HAL