Actualités et événements
MT180s : Gaspard Fougea reçoit le prix du jury à la finale Université Paris-Saclay
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.
Soutenance de thèse : Olivier Stietel
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
Soutenance de thèse : Antoine Lanco
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...
Soutenance de thèse : Alexandrina Korneva
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...
Soutenance de thèse : Nathan Thomasset
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...
PhD Defence: Giann Karlo
Ecosystem causal analysis using Petri net unfoldings
by Giann Karlo
Thursday 14 December 2023 at 9 am
ENS Paris-Saclay, Room 1Z53 and Zoom
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...
PhD Defence: Xavier Denis
Deductive Verification of Rust Programs
by Xavier Denis
Monday 18 December 2023 at 2pm
Batiment 660, Amphitheatre and video conferencing Zoom link.
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...
Best-Paper Award at JELIA 2023
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...
LICS 2023 Test-of-Time Award pour Hubert Comon-Lundh
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.
Hubert Comon-Lundh receives LICS 2023 Test-of-Time Award
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