News & Events

Toutes nos félicitations à Gaspard Fougea pour le prix du jury reçu à la finale Université Paris-Saclay du concours Ma thèse en 180 secondes.

Gaspard prépare sa thèse « Modèles formels pour la conscience : de l’expérience subjective aux algorithmes cognitifs » au LMF sous la direction d'Alain Finkel et Stéphane le Roux.

https://www.youtube.com/watch?v=SYZ5LvZieOA

Dec 14 14:00 ₂₀₂₃

Local First Order Logic with Data: Toward Specification of Distributed Algorithms

Jeudi, 14 décembre 2023, 14h00
Université Paris CIté, Bâtiment Sophie Germain, salle 3052

Read more...

Dec 15 14:00 ₂₀₂₃

Stratégies pour la réduction forte

Vendredi 15 décembre 2023 14h

Université Paris-Saclay, bâtiment 660 (amphithéâtre) et visioconférence

Résumé: La sémantique d’un langage de programmation, et d’un langage fonctionnel en particulier, laisse généralement une certaine liberté quant à l’ordre dans lequel sont effectuées les différentes opérations. Les différentes stratégies qui peuvent être adoptées, comme l'appel par valeur ou l'évaluation paresseuse, bénéficient déjà à la fois d'un large corpus théorique et de nombreuses implémentations efficaces. Ce corpus cependant est majoritairement tourné vers un objectif d'évaluation des programmes, c'est-à-dire de production d'une valeur. Le cadre associé est celui de l'évaluation faible, dans lequel aucune évaluation n'est effectuée à l'intérieur d'une fonction qui ne serait pas totalement appliquée. En effet, dans un langage fonctionnel la fermeture représentant une telle fonction est déjà en elle-même considérée comme une valeur. Read more...

Dec 8 10:30 ₂₀₂₃

The Cubicle Fuzzy Loop: A Testing Framework for Cubicle

Vendredi 8 décembre 2023 10h30

Université Paris-Saclay, bâtiment 650, salle 435 (salle des thèses)

Résumé. L’objectif de cette thèse est d’intégrer une technique de test dans le model checker Cubicle. Pour cela, nous avons étendu Cubicle avec une boucle de Fuzzing (appelée Cubicle Fuzzy Loop – CFL). Cette nouvelle fonctionnalité remplit deux fonctions principales. Tout d’abord, elle sert d’oracle pour l’algorithme de génération d’invariants de Cubicle. Ce dernier, basé sur une exploration en avant de l’ensemble des états atteignables, était fortement limité par ses heuristiques lorsqu’elles sont appliquées à des modèles fortement concurrents. Read more...

Dec 21 14:00 ₂₀₂₃

Stratégies à mémoire finie dans les jeux concurrents à deux joueurs.

Jeudi 21 décembre 2023 à 14h00
ENS Paris-Saclay, Salle 1Z71, zoom

Résumé. On étudie des jeux concurrents à deux joueurs de durée infinie qui se jouent de la façon suivante : chaque tour, les deux joueurs choisissent chacun une action sans connaître le choix actuel de l'adversaire. Sur un nombre de tours infini, cette procédure génère une suite infinie de paires d'actions. Cette suite est alors gagnante pour le Joueur 1 si elle appartient à l'ensemble gagnant du jeu. Read more...

Dec 14 9:00 ₂₀₂₃

Abstract. Many verification problems for concurrent systems have been successfully addressed by various methods over the years, particularly Petri net unfoldings. However, questions of long-term behavior and stabilization have received relatively little attention. For instance, crucial features of the long-term dynamics of ecosystems, such as basins of attraction and tipping points, remain difficult to identify and quantify with good coverage. Read more...

Dec 18 14:00 ₂₀₂₃

Abstract. Rust is a programming language introduced in 2015, which provides the programmer with safety features regarding the use of memory. The goal of this thesis is the development of a deductive verification tool for the Rust language, by leveraging the specificities of its type system, in order to simplify memory aliasing management, among other things. Read more...

Stéphane Demri (LMF, CNRS) and Karin Quaas (Leipzig University) received the Best-Paper Award at JELIA 2023, the 18th Edition of the European Conference on Logics in Artificial Intelligence, which is a major forum for logic-based approaches to AI. Read more...

Hubert Comon-Lundh a reçu le LICS Test-of-Time Award 2023 pour l'article Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or (ArXiv preprint) cosigné avec Vitaly Shmatikov (SRI International). Le prix a été partagé avec l'article connexe An NP Decision Procedure for Protocol Insecurity with XOR de Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch et Mathieu Turuani.

Read more...

Hubert Comon-Lundh received the LICS Test-of-Time Award 2023 for the article Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or (ArXiv preprint) co-authored with Vitaly Shmatikov (SRI International). The award was shared with the related paper An NP Decision Procedure for Protocol Insecurity with XOR by Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani.

Cryptographic protocols rely on cryptographic primitives to achieve goals such as data privacy and data authenticity in the presence of an attacker. Their use in important applications such as communications over the Internet or credit card payments calls for the automated verification of their security. These two papers made important progress on algorithmic aspects of protocol verification with additional operators, including XOR which is widely used in real-life applications.

Specifically, these papers establish the decidability of insecurity of cryptographic protocols with XOR and other equational theories. Chevalier et al. prove membership in NP when restricted to XOR, while Comon and Shmatikov prove decidability in a broader setting. In addition to definitively settling the complexity question for these cases, the lasting value of this line of work is demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.— Jury Laudation

Read more...