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

“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 ₂₀₂₂

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