Bienvenus sur la page du séminaire du département d'informatique de l'ENS de Lyon pour l'année 2023/2024, 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 !
Contact : Michele Pagani, michele.pagani@ens-lyon.fr
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.
10/04/2024 : Chien-Chung Huang, Matroid-Constrained Maximum Vertex Cover
Abstract: 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 ?
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
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
Abstract: 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
Abstract: 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
Abstract: 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
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
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!
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
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
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.