Bienvenus sur la page du séminaire du département d'informatique de l'ENS de Lyon, autrement appelé SIESTE.
Le séminaire est ouvert à tous ! Il est obligatoire pour les L3 et recommandé pour les M1. Ce séminaire vise à donner une introduction à des domaines de recherche actuels de l'informatique d’une manière accessible aux non spécialistes et aux étudiants. Même les chercheurs expérimentés peuvent être intéressés !
Horaire et lieu : mercredi 13h30-14h30, amphi B Campus Monod
L'amphi B est au 3ème étage du bâtiment principal du Campus Monod. Des rafraîchissements seront ensuite proposés à coté de l'amphi pour permettre au public de discuter avec l’orateur.
12/11/2025 : Laurent Jacques
19/11/2025 : Melissa Rossi
26/11/2025 : Antoine Amarilli
3/12/2025 : Remy Grunblatt
10/12/2025 : Yassine Hamoudi
28/01/2026 : Karoliina Lehrinen
4/02/2026 : Stefano Zacchiroli
25/02/2026 : Laurent Feuilloley
23/04/2025 : Patrick Baillot
Logique et types pour la confidentialité différentielle.
Résumé : La confidentialité différentielle (differential privacy) est une méthode pour exprimer et garantir des propriétés de protection de la vie privée dans les calculs sur des données sensibles, par exemple des données médicales. Intuitivement un programme interrogeant une base de données est différentiellement confidentiel si la présence ou l'absence d'un individu dans cette base de donnée n'a qu'un effet statistique négligeable sur son résultat. Même si de nombreux algorithmes différentiellement confidentiels ont été conçus pour une large variété de problèmes, vérifier qu'un programme donné satisfait cette propriété reste une tâche difficile. Des méthodes logiques ont donc été développées dans ce but, s'appuyant sur la logique de Hoare ou sur les systèmes de types. Cette présentation sera consacrée à une introduction à ces méthodes. Nous montrerons notamment comment la logique linéaire permet de définir un système de types pour un langage fonctionnel garantissant qu'un programme bien typé est différentiellement confidentiel.
19/03/2025 : Baptiste Lepers
Concurrence relâchée, mais concurrence prouvée.
Résumé :
Cette présentation portera sur plusieurs contributions dans le domaine des systèmes d’exploitation, avec un accent particulier sur la détection de bugs dans des environnements concurrents et (si le temps le permet) l’optimisation des performances des bases de données.
Traditionnellement, un programme utilise des verrous pour assurer l'intégrité de ses données dans un contexte multi-thread. Nous verrons que de plus en plus d'applications s'éloignent de cette approche pour des raisons de performance. Nous explorerons les challenges liés à la concurrence sans verrou et les bugs associés. Linux sera pris en exemple, et nous explorerons quelques exemples bugs critiques liés à l'absence de verrou -- et comment les détecter automatiquement.
Si le temps le permet, dans un second volet, nous explorerons les limites des bases de données sur les systèmes de stockage NVMe SSD modernes. Nous verrons que les bases de données sont limitées par leur CPU et ne savent pas exploiter les disques de manière efficace. Nous verrons comment concevoir des bases de données plus rapides.
12/02/2025 : Guillaume Baudart
Des langages de programmation probabilistes pour le raisonnement Bayesien. (Slides de l'exposé)
Résumé :
La programmation probabiliste est un paradigme qui a connu un essor important ces dernières années.
Un programme probabiliste manipule des variables aléatoires qui peuvent être conditionnées par des observations statistiques.
Des méthodes d'inférence automatiques permettent ensuite de calculer la distribution décrite par un programme.
Les langages probabilistes sont aujourd'hui utilisés dans des domaines allant de la vision par ordinateur et la robotique à la santé et aux sciences sociales.
Dans cet exposé, je présenterai les bases de la programmation probabiliste avant d'illustrer quelques développement récents à l'intersection de plusieurs domaines: sémantique, analyse statique et apprentissage automatique.
05/02/2025 : Sophie Quinton
Quelle recherche en informatique face à l'urgence écologique ?
Résumé : On imagine souvent la neutralité comme une condition sine qua non de la bonne science, indispensable sous peine de la détourner à des fins intéressées ou militantes. Pourtant, l'histoire et la philosophie des sciences ont montré que les valeurs des chercheurs, c'est-à-dire leurs attitudes fondamentales à propos de ce qui est important, bon et juste, influencent les connaissances qu'ils produisent. Dans cet exposé, nous illustrerons cette influence par différents exemples liés à la recherche en informatique. Nous discuterons ensuite des conséquences, que ce soit en termes de pratiques ou de choix des sujets de recherche, de cette impossible neutralité scientifique qu'il s'agit d'assumer. Nous nous nous intéresserons en particulier aux recherches en lien avec l'urgence écologique et nous présenterons un nouveau champ de recherche interdisciplinaire en train d'émerger, à l'intersection de l'informatique et du champ des STS (Sciences et Techniques en Société).
18/12/2024 : Mathurin Massias (Slides de l'exposé)
Le machine learning en 2024: perspectives et défis au delà des buzzwords
Résumé :
Dans de nombreuses tâches, des modèles mathématiques obtiennent maintenant des performances supérieures à celle de l'humain. ChatGPT, Dall-e ou Midjourney ont achevé de faire entrer l'intelligence artificielle dans la sphère publique, et l'on entend régulièrement parler de "singularité" et d'"intelligence artificielle générale". La machine peut-elle et va-t-elle remplacer l'humain ?
Dans cet exposé, nous aborderons les bases mathématiques du machine learning pour clarifier les raisons de ses succès récents, leur impact, et les défis qu'ils posent pour les années à venir.
27/11/2024 : Christine Solnon
La programmation par contraintes illustrée
Résumé :
Selon Freuder, « Constraint programming represents one of the closest approaches computer science has yet made to the Holy Grail of programming: the user states the problem, the computer solves it. »
Dans cette présentation, nous introduirons les principes de base de la programmation par contraintes à travers un exemple fil rouge, à savoir le problème d’isomorphisme de sous-graphe visant à rechercher une copie d’un graphe motif dans un graphe cible. Nous verrons tout d’abord comment modéliser ce problème très simplement en termes de contraintes. Nous verrons ensuite comment améliorer les performances de l’algorithme de résolution en ajoutant divers ingrédients (contraintes redondantes, propriétés invariantes, heuristiques d’ordre, restarts et inférence de nogoods, etc).
06/11/2024 : Denis Merigoux (Slides de l'exposé)
Les langages dédiés comme cheval de troie des méthodes formelles
Résumé :
La vérification de programme consiste en l'analyse d'un programme informatique vu comme un artefact formel, afin de prouver l'absence de certaines catégories de bogues avant l’exécution. Mais pour utiliser un framework de vérification de programmes, il faut auparavant traduire le code source originel du programme dans le langage formel du framework. De plus, il est possible d'utiliser plusieurs frameworks de vérification pour prouver des propriétés de plus en plus spécialisées à propos du programme.
Pour répondre au besoin de traductions multiples du programme source vers différents frameworks de vérification de programmes ayant chacun leur paradigme de preuve, je défends l'utilisation de langages dédiés orientés vers la preuve. Ces langages dédiés devraient être pensés comme une sur-couche au-dessus des frameworks de preuves, avec un design qui incorpore et distribue les obligations de preuves entre les prouveurs. De plus, le programme originel est souvent déjà traduit depuis des spécifications d'exigences informelles liées au domaine d'activité afférent. Afin de raffermir le maillon le plus haut de la chaîne de confiance, nous soutenons que les langages dédiés orientés vers la preuve peuvent aider les experts du domaine à relire la spécification du programme, spécification à la base d'ultérieurs développements d'implantations vérifiées.
En guise d'illustrations, deux exemples de langages dédiés pour calculer les impôts : Mlang est un compilateur pour un langage dédié aux calculs fiscaux utilisé par la DGFiP ; Catala est un nouveau langage qui permet l'encodage de spécifications législatives dans un code source exécutable et analysable.
23/10/2024 : Christophe Vuillot (Slides de l'exposé)
L'ordinateur quantique à l'épreuve des erreurs
Résumé :
Un ordinateur quantique parfait pourrait résoudre certains problèmes, comme la factorisation d'entiers, bien plus vite que les ordinateur classiques en l'état actuel des connaissances. De nombreux efforts sont en cours pour construire de telles machines mais nous sommes loin des ordinateurs quantiques idéaux. La raison: les erreurs qui émaillent tous les processus et réalisations physiques de qubits (bits quantiques). Le domaine de la correction d'erreur quantique et de la tolérance aux fautes explore les remèdes possibles, ou comment faire du calcul sans erreurs à partir de composants tous imparfaits.
Dans cet exposé nous verrons les principes de la correction d'erreur quantique et comment ils permettent le calcul quantique parfait avec un surcoût matériel. Nous évoquerons aussi le cas où les systèmes physiques sous-jacents ne sont pas des qubits mais des systèmes physiques plus complexes et comment le domaine de la correction d'erreur s'y applique également.
16/10/2024 : Daria Pchelina (Slides de l'exposé)
Quand les ordinateurs viennent au secours des géomètres : des arrangements de disques et des empilements de sphères optimaux
Résumé :
Comment empiler un nombre infini d'oranges pour maximiser la proportion de l'espace couvert ? Kepler a conjecturé que l'empilement des "balles de canon" est optimal. 400 ans se sont écoulés avant que cette conjecture soit démontrée par Hales et Ferguson dont la preuve comporte 6 papiers et des dizaines de milliers de lignes de code informatique.
Comment arranger un nombre infini de pièces de monnaie de 3 rayons différents sur une table infinie pour maximiser la proportion de la surface couverte ? Un arrangement de disques est dit triangulé si chacun de ses "trous" est borné par trois disques tangents. Connelly a conjecturé que si de tels arrangements existent, l'un d'eux maximise la proportion de la surface couverte; cela est vrai pour les arrangement unaires et binaires.
Dans cette exposé, nous nous intéresserons à diverses techniques utilisées dans la preuve de la conjecture de Kepler ainsi que dans d'autres résultats importants du domaine des arrangements de disques et de sphères. Elles nous permettent de prouver l'assertion de la conjecture de Connelly pour 31 triplets de rayons de disques triangulés et de la réfuter pour 45 autres triplets. De plus, nous obtenons une borne sur la densité des empilements à 2 sphères en 3D.
10/04/2024 : Chien-Chung Huang,
Matroid-Constrained Maximum Vertex Cover
Résumé : We introduce the problem of Matroid-Constrained Vertex Cover: given a graph with weights on the edges and a matroid imposed on the vertices, our problem is to choose a subset of vertices that is independent in the matroid, with the objective of maximizing the total weight of covered edges. This problem is a generalization of the much studied "max $k$-vertex cover" problem, in which the matroid is the simple uniform matroid. This problem is APX-hard and also W[1]-hard (with k, the rank of the matroid, being the paramter). Nonetheless, in this work, by two different techniques, we are able to design Fixed-Parameter Tractable Approximation Schemes (FPT-AS) for this problem.
03/04/2024 : Florent Koechlin
Comment montrer qu'un langage algébrique est intrinsèquement ambigu ?
Résumé : Une grammaire hors-contexte est non ambiguë si tout mot de son langage est reconnu par une unique dérivation. Contrairement aux automates finis, où l'expressivité des automates déterministes, non ambigus et non déterministes coïncide, chez les grammaires hors-contexte, ces trois classes sont bien distinctes: il existe ainsi des langages algébriques qui ne sont reconnus par aucune grammaire non ambiguë. Ces langages sont appelés intrinsèquement ambigus. Montrer qu'un langage algébrique est intrinsèquement ambigu est une question difficile : il faut arriver à montrer que toute grammaire hors-contexte qui le reconnaît est forcément ambiguë. Dans cet exposé, je présenterai un aperçu des différentes techniques qui sont à notre disposition pour aborder ces questions, en particulier les séries génératrices.
27/03/2024 : Oana Goga
Measuring and mitigating risks with online platforms
Résumé : In this talk, I will discuss risks associated with online platforms and present methodological approaches for measuring and mitigating these risks. I will provide insights from some of our latest results on exposure to misinformation, filter bubbles, and political ad micro-targeting.
20/03/2024 : Anne Canteaut
Vers une cryptographie minimaliste
Résumé : Le chiffrement symétrique est utilisé pour protéger la confidentialité de l'information dans la plupart des applications. L'algorithme standard, AES, offre depuis près de 25 ans un niveau de sécurité très satisfaisant, mais il n'est pas adapté aux environnements dans lesquels les ressources sont limitées (en matériel, en énergie...). Nous verrons que cette situation a fait émerger de nouvelles familles de chiffrements à bas coût, dont la conception, plus simple, soulève de nombreuses questions de recherche, algorithmiques et mathématiques.
13/03/2024 : Rob Bisseling
Parallel computations for verifying the binary Goldbach conjecture
Résumé : The binary Goldbach conjecture states that every even number larger than two can be written as the sum of two prime numbers. The conjecture is an open problem in mathematics since 1742. Its truth has been verified for even numbers up to 4 x 10^18 in April 2012, but a proof has not yet been found. We will present a new algorithm for verifying the conjecture, which is based on the use of a suitable sparse data structure, exploitation of repeating patterns in the prime numbers, and several techniques from the area of combinatorial scientific computing, in particular for solving the hypergraph vertex cover problem. Furthermore, we harness parallel computers to reach the high numbers we are interested in. Let's see how far we can get!
14/02/2024 : Omar Fawzi
Quantum computing in the presence of noise
Résumé : After a brief overview of quantum information science, I will focus on quantum error correcting codes which encode information in a well-chosen manner to be robust to local imperfections. I will introduce the formalism of quantum stabilizer codes focusing on so-called Low-Density Parity-Check (LDPC) quantum codes and give a high-level overview of some code constructions and efficient decoding algorithms.
10/01/2024 : Isabelle Guérin-Lassous (Direction LIP)
Présentation du LIP
6/12/2023 : Louis Esperet
Test de propriété dans les graphes
Résumé : Cet exposé sera une introduction à la notion de test de propriété dans les graphes. On considère un graphe G immense, et on veut décider s'il satisfait une certaine propriété P (par exemple est-il biparti ? sans-triangle ?). Le problème est que le graphe est tellement grand qu'on ne peut pas se permettre de lire toute l'entrée (en fait on ne peut que regarder quelques parties de l'entrée au hasard, et on doit répondre à la question en se basant uniquement sur ce qu'on a lu). Dans ce cadre il est impossible de répondre parfaitement à la question, et on doit se contenter de quelque chose de plus faible : on veut juste savoir faire la différence entre :
22/11/2023 : Xavier Urbain
Les essaims de robots mobiles autonomes et leur vérification
Résumé : Je présenterai quelques résultats et travaux dans le cadre des essaims de robots mobiles autonomes. Dans ce modèle assez récent, les robots déterminent leurs actions de façon totalement autonome en fonction de leur propre perception de l'environnement. Extrêmement dynamiques et versatiles, ils laissent envisager de nombreuses applications : exploration de zones dangereuses, établissement de réseaux dynamiques, etc. La vérification formelle des protocoles distribués de ce contexte, nécessaire dans les scénarios critiques, est également source de formidables défis. J'esquisserai comment nous tentons de les relever en développant le cadre formel mécanisé Pactole. Proposé pour l'assistant à la preuve Coq, ce dernier permet d'établir non seulement la correction fonctionnelle de protocoles pour essaims de robots mais aussi l'impossibilité de réaliser certaines tâches.
8/11/2023 : Pierre-Evariste Dagand
Functor-oriented programming: look Ma, no loops!
Résumé : If you run the command `ocaml` in a VT100-compatible terminal and pay very close attention to the static noise in your headphones, you are likely to hear John Backus' primal scream traveling through time (1977) and space (Seattle, USA): "Can programming be liberated from the von Neumann style?" Yet, when tasked with manipulating inhabitants of `Array.t` or some of the numerous instances in `Bigarray`, we set our playlist to "Rage against the Machine" and resort to for-loops (or their 90's equivalent: iterators). Could array processing be liberated from the von Neumann style too? In particular, could we use algebra to bear on the problem? This talk is a programming riff in Agda, based on a paper entitled "APLicative Programming with Naperian Functors" by J. Gibbons.
25/10/2023 : David Monniaux
Optimizations and security additions in a formally verified compiler
Résumé : CompCert is a formally verified compiler. "Formally verified" means that there is a mathematical proof that the execution of the source matches that of the assembly code, and this proof has been checked by a proof assistant (here, Coq). It however provided limited optimization. We have since then implemented a variety of optimizations (scheduling, strength reduction across loop iterations…) that significantly reduce the gap compared to GCC. We also implemented a back-end for the Kalray KVX VLIW manycore processor. I will discuss these optimizations as well as added security features.
11/10/2023 : Romain Michon
High-Level Programming of FPGAs for Real-Time Audio Signal Processing Applications
Résumé : FPGAs offer a wide range of new exciting possibilities for real-time audio signal processing applications such as ultra-low audio latency, management of large numbers of parallel audio channels, audio computations at a high sampling rate, spatial audio, etc. However, programming them in this context remains a relatively hard task which is out of reach to most DSP engineers, hobbyists, etc. As part of the FAST project (Fast Audio Signal-processing Technologies on FPGA) we (the INRIA Emeraude Team) are developing a toolchain to program FPGA platforms for real-time audio applications using the Faust programming language, with applications for active control of room acoustics as an aim. In this presentation, an overview of this new system and of what it has to offer will be given. We'll also discuss the limitations of the use of High Level Synthesis (HLS) in the context of real-time audio DSP.