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.

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.

Synthesis for Games of Imperfect Information under Full-Information Protocols

Jul 7 14:00 ₂₀₂₅

Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B36

Abstract: Different models can be used to represent programs, to check their correctness, or even better to synthesise them from a specification. Here, we model a program as a player against an environment. Constructing a correct program then boils down to synthesising a winning strategy in the associated game, that is, a behaviour that ensures that the winning condition is satisfied regardless of the behaviour of the environment.

We introduce a new class of games where the player receives imperfect information by communicating with passive observers in a full-information protocol. Unlike the classical model, the player can in one moment obtain an unbounded amount of information.

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.

Aliaume Lopez received the 2024 E. W. Beth Dissertation Prize for his thesis First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions.

The prize, named in honor of the Dutch mathematician Evert Willem Beth, was established in 1998 by the Association for Logic, Language, and Information (FoLLI) and is awarded annually for outstanding dissertations in the fields of Logic, Language, and Information.

Aliaume prepared his thesis under the joint supervision of Jean Goubault-Larrecq at LSV, then LMF, and of Sylvain Schmitz at IRIF.

Each year, the French Academy of Sciences awards nearly eighty prizes covering the entire specrum of fundamental and applied sciences. At the award ceremony of 26 November, 2024, Gilles Dowek was bestowed with the Medal for Contributions to the History and Philosophy of Science.

Gilles Dowek explores new philosophical questions raised by the development of computer science. These questions address the role of computation in defining mathematical truth, the relationship between the Church-Turing thesis and Galileo's principle that the Universe is written in the language of mathematics, the concept of formal languages and their connection to writing, and the construction of an ethics of computer science.

— Award citation

The Medal for Contributions to the History and Philosophy of Science is awarded to an active scientist of any nationality working in a French public or private research laboratory who has contributed particularly promising results to the development of their discipline, without restriction on the fundamental or applied nature of their research.

Photo credit: © Académie des sciences – Mathieu Baumer