Launching LMF - the Formal Methods Laboratory

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.

Start-up ’’innatelogic’’ selectionné pour RISE - CNRS Innovations

RISE - CNRS Innovations

Le projet innatelogic, porté par Benedikt Bollig, Matthias Függer et Thomas Nowak, a été sélectionné pour faire partie de la prochaine promotion du programme RISE de CNRS Innovation. RISE accompagne, pendant un an, des projets de startup deeptech exploitant une technologie issue d'un laboratoire du CNRS.

Dans la quête de la prochaine génération de circuits en biologie synthétique, l'objectif d'innatelogic est de développer des logiciels innovants, basés sur l'intelligence artificielle, pour la découverte automatisée de modèles biochimiques. Ces modèles servent à optimiser les processus de la bio-production et à développer de nouveaux produits en pharmacocinétique.

Plus sur le projet "innatelogic"..

Philippe Schnoebelen receives LICS 2022 Test-of-Time Award

Philippe Schnoebelen

Philippe Schnoebelen receives the LICS Test-of-Time Award 2022 for the article Temporal Logic with Forgettable Past co-authored with François Laroussinie (Université Paris-Cité) and Nicolas Markey (IRISA, CNRS). At the time of the writing of the article in 2002, the three authors were members of the same laboratory LSV which integrated the LMF in 2021.

The LICS - Logic in Computer Science conference is the most prestigious annual forum on theoretical and practical topics in computer science related to logic in a broad sense. The LICS Test-of-Time Award award recognizes a small number of papers from the LICS proceedings over the past 20 years (i.e., the paper in question dates from LICS 2002 and was considered this year) that have best stood the "test of time." In selecting these papers, the award committee considers the influence they have had since their publication; due to the fundamental nature of LICS work, the impact is often not felt immediately, hence the 20-year perspective.

Lasting impact on the foundations of automatic verification

According to the awarding jury, "This extraordinarily clear and elegant paper provides well-motivated and complete characterizations of succinctness and complexity of linear temporal logic with past operators and with forgettable past. It has contributed to spur a vibrant research program on logics and automata over infinite alphabets, from hardness results to the translations of logical formulas into alternating register automata, along with the attendant powerful algorithmic consequences for model checking. It has also strongly influenced the development of the field of nominal computation, and it is no exaggeration to state that the present paper has tangibly led to a number of invited talks, Dagstuhl-type workshops, research grants, academic positions, and prizes, and continues to have an ongoing and lasting impact in the areas of automata theory and the foundations of automated verification."

The award will be presented at the conference awards session LICS 2022 organized from August 2 to 5 in the framework of FLOC 2022 -- Federated Logic Conference in Haifa, Israel.

Algorithm for consistent query answering under primary key constraints

Speaker: Anantha Padmanabha, ENS Ulm.

Tuesday May 10 2022, 11:00, (salle 1Z76 ENS Paris-Saclay and online)

Abstract: Databases often have constraints. However, these days it is common to have databases that violate such constraints. Such a database is called an “inconsistent database”. One of the basic constraints is the “primary key constraint” which states there can be at most one tuple for every primary key. If a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q, is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, we have a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete.

The conjecture is open in general, but has been verified for self-join-free and path queries. However, the polynomial time algorithms known in the literature are complex and use different strategies in the two cases. We propose a simple inflationary fixpoint algorithm for consistent query answering which correctly computes certain answers when the query q falls in the polynomial time cases for self-join-free queries and path queries. This raises a natural question, whether this algorithm works for all polynomial time cases. We answer this negatively and show that there are polynomial time certain queries (with self-joins) which cannot be computed by such an algorithm.

This is a joint ongoing work with Diego Figueira, Luc Segoufin and Cristina Sirangelo.

PhD Defence: Gabriel Hondet

Expressing Predicate Subtyping in Computational Logical Frameworks
by Gabriel Hondet
Tuesday 27 September 2022 at 5pm
ENS Paris-Saclay, Room 1Z14

Abstract: Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Predicate subtyping extends simple type theory by allowing terms to be defined by predicates. A predicate subtype { x : A | P(x) } is inhabited by terms t of type A for which P(t) holds. This extension provides a rich and intuitive but undecidable type system.


Prix Doctorants STIC du plateau de Saclay pour Pierre Vandenhove

Pierre Vandenhove est lauréat d'un accessit au Prix « Doctorants » du plateau de Saclay dans la domaine STIC - Sciences et Technologies de l'Information et la Communication.

Le prix "Meilleure production scientifique en STIC du plateau de Saclay" soutenu par le LabEX DigiCosme récompense chaque année les travaux de recherche de doctorants de l’École doctorale STIC de l’Université Paris-Saclay et de l’École doctorale IP Paris pour leur excellence. L’objectif de ce prix est de dynamiser et de motiver les doctorants en les récompensant et en exposant leurs travaux à la communauté, en particulier aux jeunes chercheurs qui débutent leur thèse.


Caroline Fontaine dans Les décodeuses du numérique

La bande dessinée Les décodeuses du numérique vient de sortir. Conçu par l'INS2I du CNRS, l'ouvrage présente 12 portraits de chercheuses, enseignantes-chercheuses et ingénieures dans les sciences du numérique, illustrés par Léa Castor. Parmi les protagonistes rencontrez, dans le rôle d'agent spécial de la cybersécurité, notre collègue Caroline Fontaine.

La BD est disponible en ligne

PLDI'22 Distinguished Paper Award for Xavier Denis, Jacques-Henri Jourdan

PLDI 2022

Xavier Denis, Jacques-Henri Jourdan and their co-authors Yusuke Matsushita and Derek Dreyer received a Distinguished Paper Award for their contribution RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code at PLDI 2022, the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation.

PLDI is "the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance". It is one of the four prestigious conferences of SIGPLAN, ACM's special interest group on programming languages. Each year, among the 60-80 papers presented at the conference, only a few are selected to receive the distinguished paper award, based on their quality, and RustHornBelt is one of them for the year 2022!