Bienvenus sur la page du séminaire du département d'informatique de l'ENS de Lyon pour l'année 2024/2025, aussi 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. Mais les chercheurs expérimentés peuvent aussi être intéressés et sont bienvenus !
Contact : Yannick Zakowski, yannick.zakowski@inria.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.
06/11/2024 : Denis Merigoux
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.
27/11/2024 : Christine Solnon
La programmation par contraintes illustréeRé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).
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.