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
Download the 2023 laboratory report HERE
Contact
Director: Patricia Bouyer-Decitre
lmf-contact@lsv.fr