News

Charlie Jacomme, ancien doctorant du LSV, est lauréat du Prix de thèse 2021 du GDR Sécurité pour sa thèse Proofs of Security Protocols - Symbolic Methods and Powerful Attackers.

Mar 4 10:00 ₂₀₂₁

Abstract: Digital filters have numerous applications, from telecommunications to aerospace. To be used in practice, a filter needs to be implemented using finite precision (floating- or often fixed-point arithmetic). Resulting rounding errors may become especially problematic in embedded systems, where tight time, space, and energy constraints mean that we often need to cut into the precision of computations in order to improve their efficiency. Moreover, digital filter programs are strongly iterative: rounding errors may propagate and accumulate through many successive iterations.

As some of the application domains are critical, I study rounding errors in digital filter algorithms using formal methods to provide stronger guaranties. More specifically, I use Coq, a proof assistant that ensures the correctness of this numerical behavior analysis. I aim at providing certified error bounds over the difference between outputs from an implemented filter (computed using finite precision) and from the original model filter (theoretically defined with exact operations). Another goal is to guarantee that no catastrophic behavior (such as unexpected overflows) will occur.

Using Coq, I define linear time-invariant (LTI) digital filters in time domain. I formalize a universal form called SIF: any LTI filter algorithm may be expressed as a SIF while retaining its numerical behavior. I then prove two theorems that allow us to analyze this numerical behavior. This analysis also involves the sum-of-products algorithm used during the computation of the filter. Therefore, I formalize several sum-of-products algorithms, that offer various trade-offs between output precision and computation speed. This includes a new algorithm whose output is correctly rounded-to-nearest. I also formalize modular overflows, and prove that one of the previous sum-of-products algorithms remains correct even when such overflows are taken into account.

Jury:

• Yves BERTOT, Directeur de recherche, Inria Sophia Antipolis-Méditerranée - Reviewer
• Éric FERON, Professor, School of Aerospace Engineering, États-Unis - Reviewer
• Jérôme FERET, Chargé de recherche, Inria Paris & DI-ÉNS, ÉNS/CNRS/Université PSL - Examiner
• Florent HIVERT, Professeur, LISN, Université Paris-Saclay - Examiner
• Mioara JOLDES, Chargée de recherche, LAAS-CNRS, CNRS Toulouse - Examiner
• Assia MAHBOUBI, Chargée de recherche, Inria Rennes-Bretagne Atlantique, LS2N CNRS, Nantes - Examiner
• Jean-Michel MULLER, Directeur de recherche, LIP, CNRS Lyon - Examiner
• Sylvie BOLDO, Directrice de recherche, Inria Saclay - Île-de-France - Thesis advisor
• Thibault HILAIRE, Maître de conférence, LIP6, Sorbonne Université - Thesis co-advisor

Renaud Vilmart illustre sa thèse dans l'article Ordinateur quantique : quand un petit dessin vaut mieux qu’un long code apparu sous la rubrique Il était une fois… ma thèse du Blog BINAIRE.

Renaud est lauréat d’un accessit au prix de thèse décerné par la SiF et patronné par l’Académie des Sciences pour sa thèse ZX-Calculs pour l’Informatique Quantique et leur Complétude.

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.

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.