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

Contributions to FHE security against CCA adversaries

Dec 10 14:00 ₂₀₂₅

Wednesday 10 December 2025 at 14h00
CEA Nano-Innov (Building 862, Amphi 33-34) and online

Abstract: Homomorphic encryption (FHE) is a cryptographic tool allowing the delegation of computations over sensitive data while preserving its confidentiality. Unfortunately, what makes the power of FHE, its malleability (the ability to perform computations over ciphertexts), is also one weak point. On their own, homomorphic schemes only provide a relatively low security guarantee (CPA security, which models passsive adversaries) in comparison to what is usually expected (CCA2 security, which models active adversaries) from more "classical" cryptosystems. Read more...

Dec 9 14:00 ₂₀₂₅

Abstract: An important question in the domain of distributed computing is that of task solvability : given a distributed task, the analog of a program specification for distributed systems, under which conditions can it be solved by some distributed protocol ? The topological approach to distributed computing represents tasks and protocols as relations between simplicial complexes, combinatorial objects which encode possible global states of the system. These have a spatial interpretation, which led to the Asynchronous Computability Theorem (ACT), which relates, for certain computational models, the existence of a continuous map to task solvability, using subdivisions of the input space.

Read more...

Precise and Efficient Memory Analysis of Low-level Languages

Dec 17 14:00 ₂₀₂₅

Wednesday 17 December 2025 at 14h00
ENS Paris-Saclay, Room 1Z61 and online

Abstract: Memory safety is crucial for systems like embedded software and operating systems, where errors such as buffer overflows or use-after-free can lead to serious security issues. This thesis presents a sound, automated, and practical static analysis to prove spatial memory safety in binary code or C programs. The method builds on a novel dependent type system called TypedC which extends C's types to express complex memory properties. It works without modifying source code and uses abstract interpretation to check types and ensure spatial memory safety. A second contribution is a new framework for building relational compositional abstract domains called AADT. It enables precise analysis of complex data types like arrays, structs, and unions. The approach is implemented in the Codex platform and tested on real-world low-level code, showing strong results in verifying memory safety. Read more...

HOL-CSP: A Comprehensive Process Theory for Semantics and Proc-Omata Reasoning

Dec 18 14:00 ₂₀₂₅

Abstract: CSP (Concurrent Sequential Processes) is a theory for concurrent computations and interaction. HOL-CSP is a conservative embedding of CSP into Higher-order logic (HOL); this gives rise to an environment that allows formal, machine-assisted proof of behaviour which is rich in data. A particular class of processes can be seen as symbolic automata whose finite instances can be treated by a model-checker. HOL-CSP is very

expressive and allows for representing finite automata and their infinite extensions as occurring for dense time, physical systems, and parameterized process architectures. 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.

In their award-winning contribution, entitled Model-checking real-time systems: revisiting the alternating automaton route, they present the first symbolic approach to the analysis of single-clock alternating timed automata, a powerful model that allows to capture rich timed properties.