Actualités et événements
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
Gilles Dowek lauréat du Grand prix Inria - Académie des sciences 2023
Le Grand prix 2023 Inria-Académie des sciences a été décerné à Gilles Dowek.
Parallèlement à ses travaux scientifiques et techniques, Gilles Dowek a contribué à la construction d'une philosophie naissante de l'informatique, qui se construit dans un dialogue entre philosophes et scientifiques. Il s'est, en particulier, intéressé à la place du calcul en mathématiques, à la différence entre les langues et les langages et aux rapports entre la thèse de Church-Turing et celle de Galilée.— Citation du prix
Le Prix Inria – Académie des sciences récompense depuis 2013 une ou un scientifique ayant contribué de manière exceptionnelle au champ des sciences informatiques et mathématiques.
PhD Defence: Georges Aazan
Stability of constrained switched systems driven by ω-regular languages
by Georges Aazan
Friday 27 October 2023 at 2pm
ENS Paris-Saclay, Room 1Z14 and Zoom
Abstract. Switched systems are dynamical systems with several operating modes, each mode being described by a differential (continuous time) or difference (discrete time) equation. Read more...
Soutenance de thèse : Clément Pascutto
Runtime Verification of OCaml Programs
Mercredi 18 octobre 2023 14h
Université Paris-Saclay, bâtiment 660, salle 40 (amphi)
Formal verification methods, in particular when it comes to deductive verification, bring strong guarantees about the correctness of software systems. However, they require a high degree of expertise and tremendous development time. Read more...
PhD Defence: Benjamin Bordais
Concurrent two-player antagonistic games on graphs
by Benjamin Bordais
Thursday 12 October 2023 at 2PM
ENS Paris-Saclay, room 1Z56
Abstract. We study two-player antagonistic games on graphs. In such a setting, two players, Player A and Player B, start at a given state of a graph and then concurrently interact to choose a probability distribution over successor states. This process is then repeated indefinitely, thus creating an infinite sequence of states: the outcome of game. That outcome is mapped by a payoff function to a value between 0 and 1 that Player A wants to maximize, while Player B wants to minimize it.
Soutenance de thèse : Aliaume Lopez
First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions
par Aliaume Lopez
Mardi 12 septembre 2023 à 14h
Université Paris-Cité, Bâtiment Olympe de Gouges, salle 127
Soutenance de thèse : Rébecca Zucchini
Bibliothèque certifiée en Coq pour la provenance des données
par Rébecca Zucchini
Mardi 4 juillet 2023 à 14h
ENS Paris-Saclay, salle 1Z14
Résumé : La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. Read more...
