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.

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

Jun 17 14:00 ₂₀₂₆

Abstract: This talk highlights some of the most fascinating aspects of the logic of hybrid games, which constitute the foundation for developing multi-agent cyber-physical systems (CPS) such as robots, cars and aircraft, with the mathematical rigor that their safety-critical nature demands. Differential game logic (dGL) provides an integrated specification and verification language for hybrid games that combine discrete transitions and continuous evolution along differential equations with adversarial dynamics resolved by different players with different objectives. dGL can be used to study the existence of winning strategies for hybrid games, i.e., ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e., one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. Read more...

Jun 2 13:00 ₂₀₂₆ Jun 3 9:00 ₂₀₂₆

GT DAAL, the Working Group on Data, Automata, Algebra, and Logic, gathers the French community working on mathematical foundations for the verification of programs and databases.

Topics include database theory, automata theory (words, trees, orders, quantitative and probabilistic models), logic (specification and query formalisms, model theory, model checking, satisfiability, containment, synthesis), games (in logic, verification, model theory, set theory), and algebra and topology. The annual meeting of GT DAAL will be held at ENS Paris-Saclay, in auditorium 1B26, on 2–3 June 2026. For information on the programme, visit https://lmf.cnrs.fr/DAAL2026/.

Vérification pratique de transformations de circuits quantiques

Jun 4 14:00 ₂₀₂₆

Jeudi 4 juin 2026 à 14h00, heure de Paris
Salle 1Z61, École normale supérieure Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette

Le lien de visioconférence et les informations pratiques seront disponibles sur la page de la soutenance : https://jricc.github.io/github.io

Résumé : Ma thèse porte sur la vérification formelle des transformations de circuits quantiques. Ces transformations sont essentielles en compilation, optimisation ou adaptation au matériel, mais elles peuvent modifier le comportement du circuit. Read more...

Jun 19 9:00 ₂₀₂₆

A colloquium in memory of Gilles Dowek (1966–2025) will be held on 19 June 2026 at ENS Paris-Saclay.

The event will bring together colleagues, collaborators, and former students to reflect on his influential contributions to computer science, logic, and philosophy. Gilles Dowek made important advances in type theory and automated reasoning, and was also deeply involved in education. The colloquium will highlight the breadth of his work and its lasting impact. Further information is available on the event webpage: https://deducteam.gitlabpages.inria.fr/colloque-gilles/

Jun 10 9:00 ₂₀₂₆

The 1st Workshop on Computational Psychology will take place on June 10th 2026 at ENS Paris-Saclay. Computational Psychology is an interdisciplinary framework that formalizes psychological processes through explicit computational structures.

Situated at the intersection of theoretical psychology, computer science, and data science, it seeks to transform psychological theories into well-defined systems capable of simulation and empirical testing. For information on the programme and registration, visit https://compsych.sciencesconf.org.

Jun 17 9:00 ₂₀₂₆ Jun 18 18:00 ₂₀₂₆

LHC is a French workgroup about logic, homotopy and categories. It brings together researchers in France who work on connecting theoretical computer science, topology, and

category theory to study the theoretical foundations of programming languages, logic, and their semantics. The seventh edition of the LHC days will take place on Wednesday 17 and Thursday 18 June 2026. For information on the programme and registration, visit https://smimram.gitlabpages.inria.fr/lhc/journees.html.

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