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.

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 10 14:00 ₂₀₂₆

Abstract: I will first discuss Verbose Lean, a teaching library where students use controlled natural language and custom automation to write proofs in Lean. The goal of this library is not to make it easy to write Lean code, the goal is to make it easy to transfer proving skills from computer to paper. This library shares many goals and solutions with the Rocq Waterproof library. Then I will discuss Informal Lean, a project with Kyle Miller to turn Lean files into interactive web pages in natural language where readers can choose the level of detail. I will also comment on how those projects interact with the current generative AI madness.

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