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.

Contact

Site web

LMF - Laboratoire Méthodes Formelles
Université Paris-Saclay, CNRS, ENS Paris-Saclay
4 avenue des Sciences
91190 Gif-sur-Yvette, France

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

Mail : lmf-contact@lsv.fr

Les dernières publications

Communication dans un congrès
06/03/2023
A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem
Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
Article dans une revue
01/02/2023
Unification of Drags and Confluence of Drag Rewriting
Jean-Pierre Jouannaud, Fernando Orejas
Communication dans un congrès
31/01/2023
Formal proofs applied to system models
Évelyne Contejean, Andrei Samokish
Communication dans un congrès
31/01/2023
Communication dans un congrès
31/01/2023
L'arithmétique de séparation
Jean-Christophe Filliâtre, Andrei Paskevich
Voir toutes les publications du laboratoire sur HAL