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.

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

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/

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.

The CNRS Silver Medal follows several distinctions she has received, including the CNRS Bronze Medal (2007), the EATCS Presburger Award (2011), and an ERC Starting Grant (2012). Patricia Bouyer-Decitre served as director of the Laboratoire Spécification et Vérification in 2020, and of the Laboratoire Méthodes Formelles from 2021 to 2025.

Further information can be found in the CNRS press release.

Jun 2 9:00 ₂₀₂₆ Jun 3 18: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 and registration, visit https://lmf.cnrs.fr/DAAL2026/.

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.