Création du Laboratoire Méthodes Formelles

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.

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

LICS Test-of-Time Award pour Philippe Schnoebelen

Philippe Schnoebelen

Philippe Schnoebelen reçoit le LICS Test-of-Time Award 2022 pour l'article Temporal Logic with Forgettable Past cosigné avec François Laroussinie (Université Paris-Cité) et Nicolas Markey (IRISA, CNRS). Au moment de la rédaction de l'article en 2002, les trois auteurs étaient membres du même laboratoire LSV qui a intégré le LMF en 2021.

La conférence LICS — Logic in Computer Science est le plus prestigieux forum annuel sur des sujets théoriques et pratiques en informatique liés à la logique au sens large. Le prix LICS Test-of-Time Award récompense un petit nombre d'articles tirés des actes du LICS des 20 dernières années (c'est-à-dire que l'article en question date du LICS 2002 et a été pris en considération cette année) qui ont le mieux résisté à "l'épreuve du temps”. En sélectionnant ces articles, le comité d'attribution tient compte de l'influence qu'ils ont eue depuis leur publication ; en raison de la nature fondamentale des travaux de la LICS, l'impact n'est souvent pas ressenti immédiatement, d'où la perspective de 20 ans.

Fondaments de la vérification automatique

Selon le jury d'attribution : “Cet article extraordinairement clair et élégant fournit des caractérisations complètes et bien motivées de la succinctivité et de la complexité de la logique temporelle linéaire avec opérateurs passés et avec passé oubliable. Il a contribué à stimuler un programme de recherche dynamique sur les logiques et les automates sur les alphabets infinis, depuis les résultats de dureté jusqu'aux traductions des formules logiques en automates à registre alternatif, avec les conséquences algorithmiques puissantes qui en découlent pour le model checking. Il a également fortement influencé le développement du domaine du calcul nominal, et il n'est pas exagéré d'affirmer que le présent article a conduit de manière tangible à un certain nombre de conférences invitées, d'ateliers de type Dagstuhl, de subventions de recherche, de postes universitaires et de prix, et continue d'avoir un impact continu et durable dans les domaines de la théorie des automates et des fondements de la vérification automatique.”

Le prix a été remis lors de la conférence LICS 2022 organisée du 2 au 5 aout dans le cadre de FLOC 2022 -- Federated Logic Conference à 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.

Read more...

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.

Read more...

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 https://ins2i.cnrs.fr/fr/les-decodeuses-du-numerique.

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!

Read more...