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

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.