The Formal Methods Laboratory (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.

Application Domains

  • Safety of software systems in transport.
  • Quantum computing
  • Programming languages
  • Toolchain compilation
  • Specification/Certification
  • Diagnosis of human behavior in accidents.
  • Proof of correctness of the "Responsibility-Sensitive Safety" strategy of driving autonomous vehicles.
  • Safety of real-time and hybrid systems: manufacturing processes, transport systems and communication networks.
  • Safety of dynamic systems controlled by neural networks: transport systems, medical systems.
  • Emotion identification by neural networks combined with rule-based inference: Therapeutic Chatbot.

Industrial Partners

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

Academic Partners

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.

Learn more

Visit the laboratory website

Download the 2023 laboratory report HERE

Contact

Director: Patricia Bouyer-Decitre
lmf-contact@lsv.fr

 

Latest submissions

Article in a review
10/15/2024
Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly
Léo Andrès, Filipe Marques, Arthur Carcano, Pierre Chambart, José Fragoso Femenin dos Santos, Jean-Christophe Filliâtre
Pre-submission / Working document
10/10/2024
Double-Logarithmic Depth Block-Encodings of Simple Finite Difference Method's Matrices
Sunheang Ty, Renaud Vilmart, Axel Tahmasebimoradi, Chetra Mang
Pre-submission / Working document
10/08/2024
Dirac quantum walk on tetrahedra
Ugo Nzongani, Nathanaël Eon, Iván Márquez-Martín, Armando Pérez, Giuseppe Di Molfetta, Pablo Arrighi
Communication on a congress
10/07/2024
Proofs on Inductive Predicates in Why3
Jean-Christophe Filliâtre, Andrei Paskevich, Henri Saudubray
Communication on a congress
09/14/2024
Browse all laboratory submissions on HAL