Awards and Honors

Patricia Bouyer-Decitre (LMF, CNRS, ENS Paris-Saclay) has been awarded the CNRS Silver Medal 2026 in recognition of her contributions to formal methods, automata theory, logic, and game theory. This prestigious distinction honors researchers for the originality, quality, and impact of a body of work that significantly advances research at the national and international levels.

The CNRS Silver Medal follows several distinctions she has received, including the CNRS Bronze Medal (2007), the EATCS Presburger Award (2011), and an ERC Starting Grant (2012). Patricia Bouyer-Decitre served as director of the Laboratoire Spécification et Vérification in 2020, and of the Laboratoire Méthodes Formelles from 2021 to 2025.

Further information can be found in the CNRS press release.

The annual program verification competition VerifyThis took place in Turin, as part of ETAPS 2026. Among 24 participating teams, two teams from LMF received prizes, including the main award:

• Best Overall Team: Li-yao Xia and Jacques-Henri Jourdan
• Best One-Person Team: Jean-Christophe Filliâtre

Read more...

Raghda El Shehaby (TU Wien, Institute of Computer Engineering), Matthias Függer (LMF, CNRS, ENS Paris-Saclay), Florian Huemer (TU Wien, Institute of Computer Engineering) and Andreas Steininger (TU Wien, Institute of Computer Engineering) received the Best IEEE ASYNC Paper Award in 2025.

In their award-winning contribution, entitled Investigating the Effects of Permanent Faults in QDI Circuits: A Formal Perspective, they present an algorithm and implementation to exhaustively detect all permanent faults in digital circuits. While the paper is focused on so-called Quasi Delay Insensitive (QDI) circuits, the method generalizes to synchronous circuits.

Patricia Bouyer (LMF, CNRS), B Srivathsan (CMI and ReLaX, India) and Vaishnavi Vishwanath (CMI, India) received the Best ETAPS Paper Award in 2025, which is given to the best theoretical paper at ETAPS, the International Joint Conferences on Theory and Practice of Software.

In their award-winning contribution, entitled Model-checking real-time systems: revisiting the alternating automaton route, they present the first symbolic approach to the analysis of single-clock alternating timed automata, a powerful model that allows to capture rich timed properties.