News

Jun 30 10:00 ₂₀₂₁

Summary: In the context of the multiplicity of formal systems, it has become a growing need to express formal proofs into a common logical framework. This thesis focuses on the use of higher-order term rewriting to embed complex formal systems in the simple and well-studied lambda-Pi calculus modulo. 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...

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.

Marie Fortin received the EATCS Distinguished Dissertation Award for 2020. The award established by the European Association of Theoretical Computer Science recognises outstanding dissertations in the field of Theoretical Computer Science.

Marie prepared her thesis Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata at LSV under the supervision of Benedikt Bollig and Paul Gastin.

Un article sur Patricia Bouyer vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.

Lire l'article

La plateforme Why3 développé au LMF est au sujet d'un article apparu dans les Actualités de l'INS2I-CNRS à la suite d'un entretien avec Jean-Christophe Filliâtre.

Lire l'article

The team of Jean-​Christophe Filliâtre and Andrei Paskevich was recognised Best overall team at this year's VerifyThis Competition. The team of Quentin Garchery and Xavier Denis won the first place for the Best student team award.

VerifyThis is a series of program verification competitions, which takes place annually since 2011. The competition offers a number of challenges presented in natural language and pseudocode. Participants have to formalise the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

Serge Haddad is co-chairing CONCUR 2021 organised as part of the QONFEST 2021 conference which federates four main venues in the area of formal methods:

• CONCUR 2021, the 32st International Conference on Concurrency Theory
• FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems
• FORMATS 2021, the 19th International Conference on Formal Modeling and Analysis of Timed Systems
• QEST 2021, the 18th International Conference on Quantitative Evaluation of SysTems

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