News & Events

ACM Software System Award for Jacques-Henri Jourdan / CompCert

Association for Computing Machinery (ACM) logo

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.

PhD Defence: Lulu He

Formal verification at design stage of diagnosis related properties for discrete event and real-time systems
by Lulu He
Wednesday 18 May 2022 at 10am
Room 435 (salle des thèses), building 650, 6 Rue Noetzlin, 91190 Gif-sur-Yvette.

Lulu He

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

Portraits de chercheurs : Stefan Haar

Stefan Haar

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

New Project on Safety in Autonomous Cars

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


Science ouverte : Prix pour Coq

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

Nouveau prix de thèse pour Charlie Jacomme

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.

PhD Defence: Igor Khmelnitsky

Verification of Infinite-State Systems and Machine Learning
by Igor Khmelnitsky
Thursday 27 January 2022 at 2pm
Room 1Z25, ENS Paris-Saclay and online

Igor Khmelnitsky

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

Soutenance de thèse : Quentin Garchery

Certification de la transformation de tâches de preuve
par Quentin Garchery
Mardi 25 janvier 2022 à 14h00
Salle 435 (salle des thèses), bâtiment 650 Ada Lovelace et en ligne

Quentin Garchery

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

Habilitation Defense: Matthias Függer

Matthias Függer

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

PhD Defense: Yaëlle Vinçont

Fuzzing et exécution symbolique pour la détection de vulnérabilités à large échelle
by Yaëlle Vinçont
Thursday 14 December 2021 at 14:00
at CEA (Nano-Innov), room 33-34 of Building 862

Yaëlle Vinçont

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

PhD Defense: Jawher Jerray

Guaranteed properties of dynamical systems under perturbations
by Jawher Jerray
Friday 10 December 2021 at 11:00
Université Sorbonne Paris Nord, LIPN, Room B107

Jawher Jerray

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.


Patricia Bouyer co-chairing FoSSaCS

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