News & Events

Jacques-Henri Jourdan receives the 2021 ACM Software System Award together with Xavier Leroy, Sandrine Blazy, Zaynah Dargaye, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan for their work on the CompCert formally verified compiler.

CompCert, initiated in 2005, is a compiler for the C programming language and the first industrial-strength compiler with a formally verified proof of correctness. It generates optimized code for most common computer architectures including PowerPC, ARM, RISC-V and x86.

The ACM Software System Award honours people or organizations "recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both". The 2021 award is endowed with a prize of $35,000 sponsored by IBM.

May 18 10:00 ₂₀₂₂

Abstract: Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the system property allowing one to determine at design stage whether a given fault occurring online will be identifiable with certainty based on the available observations, which is an alternative to testing that can only show the presence of failures without guaranteeing their absence. Read more...

Repousser les limites des systèmes à événements discrets : un article sur notre collègue Stefan Haar vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.

Lire l'article

“How can we model autonomous cars in the most general way and establish the absence of catastrophic events? How to preserve such safety properties under extensions of the model?" This question marked the beginning of a fruitful partnership with SystemX on projects like SVR and now 3SA involving industrial partners such as transdev, Renault and PSA.

Read more...

L'assistant de preuves Coq est d'abord un langage informatique qui permet d'écrire des définitions et des énoncés mathématiques, de décrire des structures de données informatiques et des algorithmes. Il s’agit aussi d’un environnement pour développer des preuves de théorèmes complètement vérifiées par l'ordinateur, par exemple, la correction d'un algorithme. Read more...

Charlie Jacomme, ancien doctorant du LSV, obtient un accessit du Prix de thèse Gilles Kahn de la Société Informatique de France (SIF) pour sa thèse Proofs of Security Protocols - Symbolic Methods and Powerful Attackers. Cette nouvelle récompense s'ajoute au Prix de thèse du GDR Sécurité attribué à Charlie en 2021.

Jan 27 14:00 ₂₀₂₂

Abstract: This work consists of three parts. The first one is devoted to the verification of Petri nets, the second one to the verification of recursive Petri nets which extend Petri nets, and the final one aims at combining active learning and verification.Read more...

Jan 25 14:00 ₂₀₂₂

Abstract: In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. Read more...

Jan 6 10:00 ₂₀₂₂

Abstract: The design and analysis of low-level computing devices directly implemented in hardware is commonly based on finite state machine models. In this work we review some of the assumptions made in these designs and discuss techniques for the cases where the assumptions fail to hold. Read more...

Dec 14 14:00 ₂₀₂₁

Abstract: The automatic generation of tests is a major issue in software engineering and security. Test suites created this way can efficiently explore the code, and find potential bugs, and therefore vulnerabilities.

In this thesis, we were interested in two of the said techniques: symbolic execution and fuzz testing. Read more...

Dec 10 11:00 ₂₀₂₁

Abstract: Dynamical systems have a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems to guarantee their correct functioning. Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their operation, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary.

In this thesis, we study dynamical systems from different perspectives and using various techniques. More specifically, we focus on the formal verification of critical properties such as schedulability, synchronization, robustness and stability.

Read more...

Patricia Bouyer is co-chairing FoSSaCS 2022 organised as part of the ETAPS 2022 conference which federates four main venues in the area of formal methods:

• ESOP 2022, the 31st European Symposium on Programming
• FASE 2022, the 25th International Conference on Fundamental Approaches to Software Engineering
• FoSSaCS 2022, the 25th International Conference on Foundations of Software Science and Computation Structures
• TACAS 2022, the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems