News

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

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

Un poste de MCF et un poste de PU à l'ENS Paris-Saclay sont ouverts dans le département d'informatique et au laboratoire LMF. Read more...