The Laboratoire Méthodes Formelles (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.

Nov 8 :00 ₂₀₂₄

A special workshop in honour of Serge Haddad on the occasion of his retirement will be held on Friday 8 November 2024 at ENS Paris-Saclay. The event is organised jointly by LMF and the Computer-Science Department of ENS Paris-Saclay.

For information on the programme and registration, visit the workshop page.

Formal Proofs in Applied Mathematics: A Coq Formalization of Simplicial Lagrange Finite Elements

Dec 9 14:00 ₂₀₂₄

Monday 9 December 2024 at 14h00
ENS Paris-Saclay, Room 1B26

Abstract. This thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts. The first part focuses on using Coq to formalize key mathematical principles such as the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral. The second part of this thesis operates within the framework of the Finite Element Method (FEM), a widely used numerical technique for solving partial differential equations (PDEs). Read more...

Exécution symbolique pour tous ou Compilation d’OCaml vers WebAssembly

Dec 16 14:00 ₂₀₂₄

Lundi 16 décembre 2024 à 14h
Amphithéâtre du bâtiment 660, Avenue des Sciences, 91190 Gif-sur-Yvette

Résumé. Les limitations de JavaScript en tant que langage par défaut du Web ont conduit au développement de WebAssembly (Wasm), un langage sûr, efficace et modulaire. Toutefois, compiler des langages à glaneur de cellules vers Wasm ne se fait pas sans peine, notamment du fait de la nécessité de réécrire le moteur d’exécution ou de la gestion des interactions avec le glaneur de cellules de l’hôte (le navigateur). Des extensions, dont WasmGC, ont été développées par les groupes de travail Wasm pour faciliter cette tâche. Nous présentons Wasocaml, le premier compilateur d’OCaml vers WasmGC. Ce projet confirme l’adéquation de la proposition WasmGC pour des langages fonctionnels et a influencé son développement. Les stratégies de compilation mises en œuvre dans Wasocaml peuvent également être appliquées à d’autres compilateurs et langages ; deux compilateurs les ont d’ailleurs déjà adoptées.Read more...

We are delighted to announce that two researchers with strong ties to our laboratory have won the Ackermann Award 2024:

🌟 Gaëtan Douéneau-Tabot

A former student at ENS Paris-Saclay, Gaëtan was recognised for his thesis, Optimization of String Transducers, supervised by Olivier Carton (IRIF, Université Paris-Cité) and Emmanuel Filiot (Université Libre de Bruxelles).

🌟 Aliaume Lopez

Aliaume completed a joint PhD between LMF and IRIF (Université Paris-Cité). His award-winning thesis, First Order Preservation Theorems in Finite Model Theory: Locality, Topology, and Limit Constructions, was supervised by Jean Goubault-Larrecq (LMF) and Sylvain Schmitz (IRIF, Université Paris-Cité).

The Ackermann Award is the Outstanding Dissertation Award for Logic in Computer Science, presented annually by the the European Association for Computer Science Logic (EACSL) during the Computer Science Logic (CSL) conference.

This year’s achievements continue a proud tradition in our laboratory, following in the footsteps of previous Ackermann Award recipients, Marie Fortin (2021) and Amina Doumane (2018).

Aliaume Lopez received the 2024 E. W. Beth Dissertation Prize for his thesis First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions.

The prize, named in honor of the Dutch mathematician Evert Willem Beth, was established in 1998 by the Association for Logic, Language, and Information (FoLLI) and is awarded annually for outstanding dissertations in the fields of Logic, Language, and Information.

Aliaume prepared his thesis under the joint supervision of Jean Goubault-Larrecq at LSV, then LMF, and of Sylvain Schmitz at IRIF.

Each year, the French Academy of Sciences awards nearly eighty prizes covering the entire specrum of fundamental and applied sciences. At the award ceremony of 26 November, 2024, Gilles Dowek was bestowed with the Medal for Contributions to the History and Philosophy of Science.

Gilles Dowek explores new philosophical questions raised by the development of computer science. These questions address the role of computation in defining mathematical truth, the relationship between the Church-Turing thesis and Galileo's principle that the Universe is written in the language of mathematics, the concept of formal languages and their connection to writing, and the construction of an ethics of computer science.

— Award citation

The Medal for Contributions to the History and Philosophy of Science is awarded to an active scientist of any nationality working in a French public or private research laboratory who has contributed particularly promising results to the development of their discipline, without restriction on the fundamental or applied nature of their research.

Photo credit: © Académie des sciences – Mathieu Baumer