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 (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. Read more...

Synthesis for Games of Imperfect Information under Full-Information Protocols

Jul 7 14:00 ₂₀₂₅

Lundi 7 juillet 2025 à 14h00
ENS Paris-Saclay, Salle 1B36 et visio

Résumé : Différents modèles peuvent être utilisés pour représenter des programmes, pour vérifier s’ils sont corrects, ou mieux pour en synthétiser à partir d’une spécification. Nous modélisons ici un programme par un joueur affrontant un environnement. Construire un programme correct revient alors à synthétiser une stratégie gagnante dans ce jeu, c’est à dire un comportement qui assure de vérifier la condition de victoire quel que soit le comportement de l’environnement.

Nous introduisons un nouveau type de jeu dans lesquels le joueur obtient une information imparfaite en communiquant avec des observateurs passifs, via un full-information protocol. Contrairement au modèle classique on peut obtenir en un instant une quantité non bornée d'information.

Nous proposons une méthode pour synthétiser des stratégies pures et randomisées dans ces jeux, applicable dès qu'un morphisme information-commutant peut être construit.

Read more...

Jun 10 14:00 ₂₀₂₅

Abstract:

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step, such that the LTL formula is satisfied. In this talk, we investigate the notion of dependent outputs in the context of reactive synthesis. Inspired by successful pre-processing techniques in Boolean functional synthesis, we define dependent outputs in reactive synthesis as outputs that are uniquely determined, given an assignment to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent outputs. Using this, we show that dependent outputs are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel framework that exploits dependent outputs in solving a synthesis problem. By implementing this framework using the widely used library Spot, we show that reactive synthesis that exploits dependent variables can solve some problems beyond the reach of existing techniques. Furthermore, we observe that among benchmarks with dependent outputs, if the count of non-dependent variables is low (≤ 3 in our experiments), our method outperforms state-of-the-art tools for synthesis.

This is joint work with S. Akshay, Eliyahu Basa and Dror Fried, and appeared in TACAS 2024.

Bio:

Supratik Chakraborty is Bajaj Group Chair Professor of Computer Science and Engineering at IIT Bombay. His research interests lie at the intersection of theoretical and applied computer science, with a focus on scalable and practical formal methods. He is a Fellow of Indian National Academy of Engineering and a Distinguished Member of ACM.

Learn Programming with OCaml is a new book by Sylvain Conchon and Jean-Christophe Filliâtre. This is an English translation (by Urmila Nair) of the French edition Apprendre à programmer avec OCaml.

The book is available as a PDF file, under the CC-BY-SA license. The source code for the various programs contained in the book is available for download, under the same license.

The book is structured in two parts. The first part is a tutorial-like introduction to OCaml through 14 small programs, covering many aspects of the language. The second part focuses on fundamental algorithmic concepts, with data structures and algorithms implemented in OCaml.

Chaque année, l'Académie des sciences remet près de quatre-vingt prix couvrant l'ensemble des domaines scientifiques, aussi bien fondamentaux qu'appliqués. Lors de la cérémonie de remise de prix du 26 novembre 2024, Gilles Dowek a reçu la Médaille d'histoire des sciences et d'épistémologie.

Gilles Dowek explore de nouvelles questions philosophiques posées par le développement de l'informatique. Ces questions portent sur le rôle du calcul dans la définition de la vérité mathématique, sur les rapports entre la thèse de Church-Turing et celle de Galilée, selon laquelle l'Univers est écrit en langue mathématique, sur la notion de langage formel et son lien à l'écriture et sur la construction d'une éthique de l'informatique. — Citation du prix

La médaille d’Histoire des sciences et d’épistémologie récompense une ou un scientifique en pleine activité de toute nationalité travaillant dans un laboratoire français de recherche public ou privé ayant contribué par des résultats particulièrement prometteurs au développement de sa discipline, sans restriction sur la nature fondamentale ou appliquée de ses recherches.

Crédit photo : © Académie des sciences – Mathieu Baumer