News & Events

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

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

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

Les journées du LMF 2021 ont eu lieux le 2 – 3 décembre au Domaine de Frémigny.

Read more...

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

Marie Fortin received the Ackermann Award 2021. The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. EACSL is the European Association for Computer Science Logic.

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.

How fast can you converge towards a consensus value?

In their recent work, Matthias Fuegger (LMF), Thomas Nowak (LISN), and Manfred Schwarz (TU Wien) study this question in distributed systems where nodes start from an initial value and seek to converge towards a common consensus value. The paper shows that deceptively simple algorithms are optimal and provides tight lower bounds.

Out now in JACM: https://dl.acm.org/doi/10.1145/3485242

Nov 17 13:30 ₂₀₂₁ Nov 18 9:00 ₂₀₂₁ Nov 19 9:00 ₂₀₂₁

Les Journées du GT Vérification du GDR IM ont lieu les 17, 18 et 19 novembre 2021 au Laboratoire Méthodes Formelles, ENS Paris-Saclay, à Gif-sur-Yvette.

Elles visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations et l'ouverture sur des thématiques liées à la vérification. Elles ont pour ambition de couvrir tous les domaines de la vérification formelle.

Pour en savoir plus