Logo du Laboratoire Méthodes Formelles (LMF)

Méthodes Formelles Lab (LMF)

The LMF Lab is the ENS Paris-Saclay's computer science laboratory of ENS Paris-Saclay, of Université Paris-Saclay and of CNRS as a joint research unit (UMR 9021).

LMF website

UMR 9021

Bâtiment Nord - ENS Paris-Saclay - Niveau 1
4, avenue des Sciences
91190 Gif-sur-Yvette
Tel. +33 (1) 81 87 54 50

Other adress:

Bâtiment 650 Ada Lovelace - Université Paris-Saclay
Rue Noetzling
91405 Orsay Cedex


  • Head: Patricia.BOUYER [at] ens-cachan.fr (Patricia BOUYER DECITRE)
  • The lab has approximately a hundred members, among which fifty permanent researchers and academics.
  • Education: Computer Science Department


In its mission to enlighten the digital world through Mathematical Logic, the LMF relies on formal methods as a tool to analyse, model, and reason about computing systems, such as computer programs, security protocols, and hardware designs. The 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.