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.

A New Scientist column  entitled "Where does time actually come from?" discusses the recent contribution by Pablo Arrighi and Gilles Dowek from LMF and Amélia Durbec from IEMN, to the somewhat fundamental questions about the nature of Time.

Read more...

Programming language and formally verified compiler for low-level numerical libraries

Nov 25 14:00 ₂₀₂₅

Tuesday 25 November 2025 at 14h00
ENS Paris-Saclay, Room 1Z76 and online

Abstract: Low-level numerical libraries like GMP and BLAS are widely used. They are mostly written in C, Fortran, and Assembly, and make a heavy use of arrays and pointers. These languages are well-suited for writing efficient code but they are not safe, that is, they have many undefined behaviors, which increase the chance for bugs. Read more...

Dec 2 14:00 ₂₀₂₅

Abstract:I am interested in verification of distributed systems with an unbounded number of agents running the same finite-state program. These include systems like conservative Petri nets, population protocols, reconfigurable broadcast networks and more. Properties of interest for these systems are "parameterized": for example, is there a number of agents N such that my system instantiated with N agents reaches a bad configuration? I will present a recent result on HyperLTL for population protocols, where we will see that the verification problem can be cast as a parameterized reachability property. I will then present some open questions for parameterized verification of such systems. If I have time, I will present my newest research direction which concerns runtime verification of distributed systems, and the hypotheses that can be made on the setting.

Causal graph rewriting: Space-time determinism and reversibility

Dec 2 10:30 ₂₀₂₅

Tuesday 2 December 2025 at 10h30
Amphi building 660 and online

Abstract: We study non-terminating graph rewriting models, whose local rules are applied non-deterministically---and yet enjoy a strong form of determinism, namely space-time determinism. For terminating computation, it is well-known that the property of confluence may ensure a deterministic end result. In the context of distributed, non-terminating computation however, confluence alone is too weak a property. In this thesis we provide sufficient conditions so that asynchronous local rule applications produce well-determined events in the space-time unfolding of the graph, regardless of their application orders.

Read more...

Permutation equivariant and permutation invariant reinforcement learning for multi-agent systems

Dec 11 9:00 ₂₀₂₅

Thursday 11 December 2025 at 9h00
ENS Paris-Saclay, Room 1Z25 and online

Abstract: Deep Reinforcement Learning (DRL) has achieved remarkable success in sequential decision-making tasks, from games to robotics. Extending DRL to Multi-Agent Reinforcement Learning (MARL) introduces additional challenges: agents must coordinate in high-dimensional environments, training becomes unstable due to non-stationarity, and learned strategies often fail to generalize across team sizes or tasks.

Read more...

Patricia Bouyer (LMF, CNRS), B Srivathsan (CMI and ReLaX, India) and Vaishnavi Vishwanath (CMI, India) received the Best ETAPS Paper Award in 2025, which is given to the best theoretical paper at ETAPS, the International Joint Conferences on Theory and Practice of Software. Read more...