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.

© Laurent Ardhuin pour le CNRS

Patricia Bouyer-Decitre (LMF, CNRS, ENS Paris-Saclay) has been awarded the CNRS Silver Medal 2026 in recognition of her contributions to formal methods, automata theory, logic, and game theory. This prestigious distinction honors researchers for the originality, quality, and impact of a body of work that significantly advances research at the national and international levels.

Read more...

Stéphane Demri, CNRS researcher at LMF, has published Concise Introduction to Alternating-Time Temporal Logics: A Guide for Understanding the Model-Checking Problem.

From the publisher’s description: ''This textbook provides a concise presentation of alternating-time temporal logics dedicated to strategic reasoning in multi-agent systems. Read more...

Oct 1 10:30 ₂₀₂₆

Abstract: Concurrent monads, due to Rivas and Jaskelioff, are a specialization of monads, namely a relaxation of lax monoidal monads (commutative monads) in ordered category theory. For the application in categorical semantics of functional programming languages, they are an abstraction of notions of effectful computation that are composable not only sequentially but also in parallel. Both the sequential and parallel compositions are unital and associative; more significantly, they are interrelated by interchange inequations. Concurrent monads categorify the ordered-algebraic concept of concurrent monoids from concurrency theory, going back to Grabowski and Gischer.

I will motivate and introduce this elegant abstraction, which treats parallel composition on a par with sequential composition, present some theory and show some examples from programming language semantics and concurrency theory.

Translations of Proofs between Higher-Order Logics and between Theories with Rewriting

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Amphi 1, Eiffel building, CentraleSupélec, Gif-sur-Yvette

Abstract: Formal proofs and proof assistants are rigorous tools for expressing theorems and verifying their validity. Formal proofs can be based on a wide variety of logics, implemented in various proof assistants, and use numerous data structures or representations. The goal of this thesis is to design translations of formal proofs between such formalisms.

Read more...

Quantum Cellular Automata and Quantum Field Theories

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Room 1B26, ENS Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette

Abstract: This thesis studies Quantum Cellular Automata (QCAs) as discrete-spacetime, strictly local, and unitary models of quantum field theories, with a focus on lattice artifacts, their resolution, and the digital quantum simulation of gauge theories.

We extend the gauged-QCA framework to non-Abelian symmetries, building the first QCA model coupling (1+1)D Dirac fermions to an SU(2) Yang–Mills gauge field.

Read more...

The annual program verification competition VerifyThis took place in Turin, as part of ETAPS 2026. Among 24 participating teams, two teams from LMF received prizes, including the main award:

• Best Overall Team: Li-yao Xia and Jacques-Henri Jourdan
• Best One-Person Team: Jean-Christophe Filliâtre

Read more...