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.

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 17 14:00 ₂₀₂₅

Abstract: Modern software and cyber-physical systems are intrinsically heterogeneous, combining discrete, continuous, probabilistic and human-in-the-loop components. Unifying Theories of Programming (UTP) provides rich, relational models of programs, supported by a refinement calculus and healthiness conditions. In contrast, Institution theory offers a logic-independent, categorical framework for heterogeneous specification and satisfaction. Yet these two influential foundations developed mainly in isolation. This talk proposes a semantic bridge between them by treating UTP theories as Institutions and wiring them together via institution (co)morphisms induced by UTP Galois connections. Signatures become UTP alphabets, sentences are healthy predicates or designs, models are programs, and satisfaction is refinement. We explore two proposals: first, replacing UTP's relational base by institutional semantics, analysing the impact on refinement, theory composition and mechanisation. Second, a hybrid framework in which UTP retains its concrete relational semantics but is organised institutionally as a "logic of logics". The outlook is a semantic "UTP supermarket" structured by institutional (co)morphisms, supporting modular, heterogeneous verification across paradigms such as reactive, probabilistic and hybrid systems and enabling tighter integration of tools like Isabelle/UTP with multi-logic environments.

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...