Séminaire SIESTE


Séminaire d'Informatique pour les Etudiants, Scientifiques, et Tous ceux que l'informatique intéresse à l'ENS Lyon

  • Public et Objectif:

    Ouvert à tous. Ce séminaire est obligatoire pour les L3, et recommandé pour les M1.
    Les types d'exposés seront variés: présentation d'un outil, survol d'un domaine de recherche, ou encore exposé scientifique par un (récent) ancien de l'école qui fera part de son expérience.

  • Contact:

    Suivi administratif du séminaire: Fatine Latif
    Organisation du séminaire: Stéphan Thomassé

  • Horaire et lieu:

    Les mardi à 13h30.
    Nous ferons le SIESTE en amphi B. Des rafraichissements seront ensuite proposés en salle passerelle du quatrième étage. Le public pourra alors discuter avec l'orateur.

  • Dates:

    9 octobre 2012. Damien Stehlé. Manipuler les réseaux euclidiens. slides

    Résumé: Un réseau est l'ensemble des combinaisons linéaires entières de vecteurs linéairement indépendants. Visuellement, le réseau forme une grille infinie de points régulièrement espacés. Les réseaux ont de nombreuses applications en informatique. Entre autres, ils apparaissent fréquemment en calcul formel, par exemple pour factoriser les polynômes à coefficients rationnels, et en cryptographie, aussi bien pour cryptanalyser que pour concevoir des protocoles. L'algorithme LLL, du nom de ses auteurs Arjen Lenstra, Hendriz Lenstra et László Lovász, permet de calculer une bonne représentation, ou base, d'un réseau donné. Cette représentation fournit de l'information intrinsèque sur le réseau manipulé. De nombreuses applications ont suivi la publication de l'algorithme LLL, et, du fait de ce succès, plusieurs accélérations algorithmiques ont par la suite été proposées. L'approche la plus efficace aujourd'hui repose, en interne, sur des calculs flottants en faible précision, donnant lieu à un algorithme hybride numérique-algébrique. Dans cet exosé, après une introduction du domaine, je décrirai l'algorithme LLL et le principe de l'accélération numérique-algébrique.

    16 octobre 2012. Louis Esperet. Utiliser la compression d'entropie pour rendre constructives des preuves existentielles.

    Résumé: Le Lemme Local de Lovász (l'autre LLL ndlr) est un outil puissant qui permet de montrer de manière très simple l'existence d'objets combinatoires avec certaines propriétés. Il affirme que si un certain nombre d'événements ont tous une petite probabilité et que ceux-ci ne sont pas trop interdépendants, la probabilité qu'aucun événement n'arrive est non nulle. Le problème était (jusqu'à une date récente) que cet outil n'était pas constructif. J'expliquerai les idées (très jolies et étonnamment simples) basées sur la compression d'entropie qui ont permis à Robin Moser d'obtenir une version algorithmique de ce lemme. Je donnerai deux exemples :
    1) Si on a une suite de listes L_1, L_2, L_3, ... à quatre éléments on peut trouver (efficacement) dans chaque liste L_i un élément a_i tel que le mot a_1 a_2 a_3 ... n'a pas de carré (i.e. de sous-mot de la forme x1 x2 ... x_k x_1 x_2 ... x_k).
    2) Toute instance de k-SAT dans laquelle chaque clause a des variables en commun avec au plus 2^(k-2) autres clauses est satisfiable (et on peut trouver une bonne assignation vrai/faux aux variables de manière efficace).

    27 novembre 2012. Manuel Bodirsky. A Short Introduction to Constraint Satisfaction Problems.

    Résumé: Many computational problems originating in various areas in theoretical computer science can be formulated as constraint satisfaction problems (CSPs). In such problems, we are given a finite set of variables and a finite set of constraints on those variables, and the task is to find an assignment to the variables that satisfies all constraints. Depending on the choice of the possible constraints, such problems might be computationally hard, or feasible. In recent years, a fascinating theory starts to emerge that provides strong criteria implying hardness, or the existence of polynomial-time algorithms for such problems. Questions that are motivated by this line of research are of central interest in finite model theory, structural combinatorics, and universal algebra. I will give a short introduction to current research on CSPs that directly leads to some of the outstanding open questions of the field.

    4 décembre 2012. Jade Alglave. Reasoning about Weak Memory.

    Résumé: Multiprocessors are now prominent, but provide execution models that are quite subtle. To write correct concurrent programs, we need formal models describing the behaviours that a multiprocessor allows or not. In this talk, I will present a class of relaxed memory models, defined in the Coq proof assistant, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests to determine properties of processor implementations. We detail the results of our experiments on Power and the model we base on them. This work identified a rare implementation error in Power 5 memory barriers.

    29 janvier 2013. Pascal Cuoq. Collaboration d'analyses dans Frama-C.

    Résumé: Frama-C est une plateforme collaborative d'analyse statique pour le langage C. Chaque technique ou idée peut être implémentée dans Frama-C sous la forme d'un greffon. Un moyen de collaboration entre greffons est par le langage de spécification ACSL : l'analyse de valeurs, un greffon d'interprétation abstraite, insère dans le programme cible des assertions ACSL pour chaque comportement non défini qu'elle est incapable d'exclure. Ces assertions peuvent être vérifiées par un autre greffon, tel qu'un greffon basé sur la logique de Hoare.

    12 février 2013. Clément Pernet. Calcul de formes normales matricielles: de l'algorithmique à la mise en pratique. slides

    Résumé: En algèbre linéaire, les formes normales fournissent des représentants uniques pour les classes d'équivalence selon différentes transformations: la forme normale de Frobenius pour la similitude dans un corps, la forme normale de Hermite pour l'équivalence dans un anneau ou de Gauss-Jordan pour l'équivalence dans un corps. Leur calcul permet en outre de révéler la plupart des caractéristiques d'une matrice, comme le rang, le profil de rang, le déterminant, les facteurs invariants, etc. De nombreux progrès ont été réalisé au cours des 20 dernières années concernant d'une part la réduction des complexités des algorithmes, et d'autre part les techniques logicielles pour des implantations efficaces. Nous présenterons une sélection de ces techniques algorithmiques et logicielles appliquées à l'élimination de Gauss, le calcul de la forme normale de Frobenius et de la forme normale de Hermite.

    19 février 2013. Corinne Touati. Quelques conséquences contre-intuitives d'une prise de décision distribuée.

    Résumé: La théorie de la décision rationnelle, et plus particulièrement sa composante distribuée, la théorie des jeux, a connu un fort développement depuis la formalisation de la notion d'équilibre par Nash dans les années 50. Ses applications en économie ont été récompensées par pas moins de 12 prix Nobel depuis les années 90. Le dernier en date (novembre 2012) a été attribué à Lloyd Shapley et Alvin Roth notamment pour leurs applications au partage de ressources. Nous allons justement dans cet exposé regarder quelques (contre-) exemples du lien entre optimisation distribuée et prise de décision (optimale) distribuée dans des problèmes d'allocation de ressources tirées d'exemples de réseaux de communications.

    19 mars 2013. Claire Mathieu. Algorithms for Optimization over Noisy Data.

    Résumé: To deal with NP-hard reconstruction problems, one natural possibility consists in assuming that the input data is a noisy version of some unknown ground truth. We present several examples, in particular correlation clustering, and transitive tournaments. In correlation clustering, the goal is to partition data given pairwise similarity and dissimilarity information, and sometimes semi-definite programming can, with high probability, reconstruct the optimal (maximum likelihood) underlying clustering. The proof uses semi-definite programming duality and the properties of eigenvalues of random matrices. The transitive tournament problem asks to reverse the fewest edge orientations to make an input tournament transitive. In the noisy setting it is possible to reconstruct the underlying ordering with high probability using simple dynamic programming.

    26 mars 2013. Jean-Sébastien Sereni. Limites de graphes denses.

    Résumé: Le but de cet exposé est de fournir une introduction à la théorie des limites de graphes denses, développée depuis 2005 principalement par Lovász et ses co-auteurs. Outre une introduction générale aux fondements de la théorie, un exemple concret d'application à un problème extrémal sera détaillé.

    2 avril 2013. David Coeurjolly. Introduction à la géométrie discrète et axe médian discret minimal. slides

    Résumé: L'objectif de la présentation sera de faire une petite introduction à la géométrie discrète et de se focaliser sur un problème combinatoire particulier : le calcul d'un axe médian discret minimal. Il s'agit de construire une représentation d'un objet discret (partie de Z^n) comme union d'un ensemble de boules discrètes (discrétisation boule euclidienne), si possible de cardinalité minimale. Ce problème a l'avantage d'être auto-suffisant et simple à décrire mais nous emmènera vers une preuve de NP-complétude "géométrique" assez amusante (bon... à minima intéressante...).

    9 avril 2013. Tom Hirschowitz. Vers une théorie des langages de programmation. slides

    Résumé: On sait de mieux en mieux raisonner sur les langages de programmation, comme en témoignent, par exemple, les récents progrès en matière de certification de compilateurs. En revanche, même si on a des méthodes, qu'on peut reproduire, on sait mal pour l'instant formaliser des résultats généraux, pouvant s'appliquer à plusieurs langages. L'exposé abordera quelques approches envisagées pour remédier à cette situation. A l'instar, quelques années plus tôt, des mathématiciens ayant défini des notions générales de groupe, anneau, etc, toutes ces approches tentent de dégager une notion générale de langage de programmation.

    16 avril 2013. Samuel Hym. Evaluation de la consommation mémoire de programme.

    Résumé: Pour éviter qu'un logiciel (en particulier dans des systèmes critiques) ne fasse d'erreurs par manque de mémoire, on veut borner la quantité de mémoire qu'il peut nécessiter. Dans de nombreux langages (tels que Java, Ocaml ou encore Javascript) les désallocations ne sont pas gérées explicitement par le programmeur: le garbage collector (GC) s'y charge d'identifier les objets morts et de récupérer leur mémoire. On verra donc dans cet exposé quelques unes des difficultés à résoudre pour obtenir un résultat suffisamment proche de la réalité. Quels problèmes engendrent exactement les GCs? Comment décomposer le problème pour arriver à traiter des programmes qui ne soient pas juste jouets? Comment traiter les nids de boucle?

  • Archives: Années 1998-2009. Attention, quelques liens manquants, d'autres archives suivront bientot.