News & Events

Oct 21 10:15 ₂₀₂₁

Abstract: As event data becomes an ubiquitous source of information, data science techniques represent an unprecedented opportunity to analyze and react to the processes that generate this data. Process Mining is an emerging field that bridges the gap between traditional data analysis techniques, like Data Mining, and Business Process Management. Read more...

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.

Caroline Fontaine has been appointed director of the CNRS Research Network on Computer Security GdR Securité Informatique in Summer 2021. The network federates the French research groups working on cryptography, formal methods for security, privacy, security of hardware, software, data and networks.

The photo shows Caroline at the International Cybersecurity Forum (FIC) on 7 - 9 September in Lille, where she presented the actions of the Network.

Gilles Dowek and Alejandro Díaz-Caro (Universidad de Buenos Aires and Universidad Nacional de Quilmes, Argentina) received the Best-Paper Award at ICTAC 2021, the 18th International Colloquium on Theoretical Aspects of Computing for their paper A New Connective in Natural Deduction, and Its Application to Quantum Computing.

Cláudio Belo Lourenço and Claude Marché from the Toccata team at LMF with co-authors from Mitsubishi Electric received the Best-Paper Award at FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems. Read more...

Jul 6 9:00 ₂₀₂₁

Jury:

• Gilles Bernot (reviewer) – Université Nice Sophia Antipolis, Polytech Nice Sophia
• Paolo Zuliani (reviewer) – Newcastle University
• Pascale Le Gall – Centrale Supélec
• Barbara König – Universität Duisburg-Essen
• Heike Siebert – Freie Universität Berlin
• Stefan Haar (PhD Supervisor) – Université Paris-Saclay

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

Sep 8 14:00 ₂₀₂₁

Abstract: Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to save more time and effort for the users.Read more...

Sep 30 14:00 ₂₀₂₁

Abstract: This thesis is at the crossroad of verification and synthesis of parameterized concurrent systems. The parameterized model checking problem asks whether a system satisfies a given specification independently of the number of its components, whereas synthesis requires an algorithmic design of protocols for its components so that the specification is satisfied.Read more...

L'Université Paris-Saclay organise une école d'été invitant les lycéennes de seconde et collégiennes de 4ème à découvrir les nouvelles sciences.

Le LMF participe à cette initiative avec une présentation des métiers de la recherche et un atelier de robotique avec capteurs. Le but de l'atelier est de concevoir quelques algorithmes distribués simples Read more...