Séminaires du LIP 2002-2003
A propos des séminaires du LIP. Comme l'année précédente, les séminaires du LIP ont lieu le mardi après-midi à 13h30 deux fois par mois avec (en principe) en alternance un exposé d'un intervenant local / un exposé d'un intervenant extérieur. La durée est de 45 minutes plus 10 à 15 minutes de questions (des modifications peuvent être envisagées si elles sont demandées à l'avance). Un pôt clôture le séminaire.
Renseignements et propositions d'exposés pour l'année 2003-2004 à : Claude-Pierre Jeannerode
Abonnement et désabonnement à la liste de diffusion : seminaire.lip "à" ens-lyon.fr
Comment se rendre à l'ENS Lyon ?
Les séminaires des années passées : 2001-2002, 2000-2001, 1999-2000.
Fin des séminaires 2002-2003, prochain séminaire : octobre 2003
Programme des séminaires...
Mardi 1er octobre 2002 à 13h30,
Amphi B (au 3ème étage)
Paul
Feautrier - Professeur ENS Lyon - Équipe
CompSys
Ordonnancement des réseaux
de processus de Kahn
Mardi 15 octobre 2002
à 13h30, Amphi B (au 3ème étage)
Stéphane
Boucheron - CR CNRS - LRI
- Équipe Algorithmes et Complexité
About the size of the
giant component in a random graph with given degree distribution
Mardi 29 octobre 2002 à 13h30,
Amphi B (au 3ème étage)
Hervé
Rivano - Étudiant en thèse à l'INRIA - Projet
Mascotte
Routage optique dans les réseaux WDM
multifibres avec conversion de longueur d'onde
Transparents de la présentation
Mardi 12 novembre 2002 à 13h30,
Amphi B (au 3ème étage)
Sébastien
Desreux - Étudiant en thèse au LIAFA - Équipe Algorithmique
et Combinatoire
Génération optimale de pavages
Transparents de la présentation: 1
2
Mardi 26 novembre 2002 à 14h00,
Amphi B (au 3ème étage)
En remplacement du séminaire initialement prévu:
Soutenance de thèse de Christope
Papazian - ÉNS Lyon - Équipe MC2
Graphes d'automates finis : Reconnaissance
& Calcul
Du 9 au 13 décembre 2002
École
d'hiver sur les systèmes complexes
Mardi 7 janvier 2003 à 13h30,
Amphi B (au 3ème étage)
Alain
Denise - Professeur au LRI
- Équipe Bioinformatique
Séquences aléatoires et analyse
des génomes
Mardi 21 janvier 2003
à 13h30, Amphi B (au 3ème étage)
Christophe
Paul - CR CNRS au LIRMM - Équipe Algorithmique
Combinatoire
Représentation implicites de graphes et
petits graphes universels
Mardi 11 février 2003 à 13h30,
Amphi B (au 3ème étage)
Gil
Utard — CR INRIA (en détachement du LaRIA) — LIP —
Équipe ReMap
Pérennité dans les systèmes
de stockage pair à pair
Mardi 4 mars 2003 à
13h30, Amphi B (au 3ème étage)
Stéphan
Thomassé — Maître de conférence au LaPCS —
Université Claude Bernard Lyon 1
Stabilité et sous-graphe minimal
fortement connexe
!
REPORTÉ À LA RENTRÉE PROCHAINE !
Nadia
CREIGNOU — Professeur au LIF — Équipe Logique et Complexité
Un théorème de classification
croisée, complexité versus transition de phase, pour les problèmes
de satisfaction de contraintes booléennes
Mardi 1er avril 2003 à 13h30,
Amphi B (au 3ème étage)
Éric
Gascard — ATER au LIFO — Université d'Orléans
Vérification formelle
d'algorithmes parallèles sur réseaux d'interconnexion symétriques
Mardi 8 avril 2003 à
13h30, Amphi B (au 3ème étage)
David
Hough — Sun Distinguished Engineer
IEEE 754R Status & Sun Microsystem Math Libraries
Mardi 15 avril 2003 à 13h30, Amphi
B (au 3ème étage)
Laurent
Théry — CR INRIA — Équipe Lemme — INRIA
Sophia Antipolis
Une visite guidée de la vérification
formelle avec l'outil de preuve Coq:
L'algorithme de Knuth pour les nombres premiers
Transparents de la présentation
Mardi 29 avril 2003 à 13h30, Amphi
B (au 3ème étage)
Clémence
Magnien — Étudiante en thèse au LIX — École
Polytechnique
Étude du modèle
du tas de sable :
points de vue algorithmique et algébrique
SÉMINAIRE
ANNULÉ
! REPORTÉ À LA RENTRÉE PROCHAINE
Nadia
CREIGNOU — Professeur au LIF — Équipe Logique et Complexité
Un théorème de classification
croisée, complexité versus transition de phase, pour les problèmes
de satisfaction de contraintes booléennes
Mardi 27 mai 2003 à 13h30, Amphi B (au 3ème étage)
Arnaud
Tisserand — CR INRIA au LIP — Équipe Arenaire
DSP : des processeurs dédiés pour le traitement numérique
du signal
Transparents de la
présentation
Mardi 10 juin 2003 à 13h30, Amphi B (au 3ème étage)
Patricia
Bouyer — CR CNRS au LSV — ÉNS Cachan
Untameable Timed Automata!
Mardi 24 juin 2003 à 13h30,
Amphi B (au 3ème étage)
Pham
CongDuc — MdC au LIP — Équipe RESO — Université Lyon
I
Multicast technology: what it is, what have been done,
what's next?
Résumés des séminaires...
Mardi 1er octobre
2002 à 13h30, Amphi B (au 3ème étage)
Paul
Feautrier - Professeur ENS Lyon - LIP
- Équipe
CompSys
Ordonnancement des réseaux de processus de Kahn
Les réseaux de processus de Kahn sont un moyen commode de spécifier des applications de type traitement du signal ou "calcul au fil de l'eau" (streaming). Ils permettent de spécifier naturellement le parallélisme et se prêtent à des représentations graphiques familières aux spécialistes du domaine. Mais le modèle de programmation associé est asynchrone et partiellement non-déterministe, alors que le modèle d'exécution sur DSP ou processeur VLIW est synchrone.
L'ordonnancement est précisémment la méthode permettant de déduire un programme synchrone d'une spécification synchrone. Il est facile d'introduire des contraintes temps-réel et d'en tenir compte de diverses façons pour calculer l'ordonnancement.
Je montrerai dans cet exposé comment étendre des algorithmes originellement développés pour la parallélisation automatique au cas des processus de Kahn. Une implémentation sera décrite. Je présenterai pour terminer l'un des nombreux problèmes encore non résolu : l'ordonnancement multidimensionnel sous contraintes de ressources.
Mardi 15 octobre 2002 à 13h30,
Amphi B (au 3ème étage)
Stéphane
Boucheron - CR CNRS - LRI
- Équipe Algorithmes et Complexité
About the size of the giant component in a random graph
with given degree distribution
Sparse random graphs with prescribed degree distribution have attracted lot of attention thanks to their relevance to web modeling. Molloy and Reed (1998) has characterized those limiting degree distributions for which the corresponding random graphs contained with overwhelming probability a giant connected component. We complement their law of large numbers by a central limit theorem: the limiting size of the giant component of random graphs with given degree distribution is Gaussian. The proof revisits the analysis of the fluctuations of the giant component for Erdös-Rényi graphs carried out in Barraez, Boucheron and Fernandez de la Vega (2000). This is a martingale-oriented analysis of a graph exploration.
Mardi 29 octobre 2002 à
13h30, Amphi B (au 3ème étage)
Hervé
Rivano - Étudiant en thèse à l'INRIA - Projet
Mascotte
Routage optique dans les réseaux WDM multifibres
avec conversion de longueur d'onde
Dans une première partie, cet exposé présentera rapidement l'évolution de la modélisation des réseaux de fibres optiques à multiplexage en longueur d'onde (WDM) et des problématiques d'optimisations que l'on peut étudier. Dans une deuxième partie, il sera question d'approximation du problème du routage optique dans les réseaux WDM « multifibres avec conversion ». Ce travail s'appuie notamment sur des améliorations des techniques d' « arrondi aléatoire » du multiflot fractionnaire, exact ou approché.
Mardi 12 novembre 2002 à
13h30, Amphi B (au 3ème étage)
Sébastien
Desreux - Étudiant en thèse au LIAFA - Équipe Algorithmique
et Combinatoire
Génération optimale de pavages
Transparents de la présentation: 1
2
Un problème de pavage, c'est la donnée d'une région du plan, généralement dans la grille carrée ou la grille triangulaire, de « tuiles », c'est-à-dire de figures géométriques élémentaires comme des rectangles ou des losanges, et d'une question: peut-on paver (recouvrir sans chevauchement) cette région avec ces tuiles ? De combien de manières peut-on le faire ? Peut-on ordonner ces pavages ? Peut-on les exhiber un par un ? Un exemple intuitif est donné par des rectangles 2*1 (appelés « dominos ») à placer sur un échiquier 8*8.
Nous proposons un algorithme optimal en temps et en espace pour générer tous les pavages d'un domaine, par des losanges ou des dominos. À cette fin, nous introduisons une généralisation de l'algorithme de Thurston, une description unifiée des pavages par des mots et une fonction successeur. L'exposé ne suppose aucune connaissance préalable sur les pavages.
Mardi 26 novembre 2002 à 14h00,
Amphi B (au 3ème étage)
En remplacement du séminaire initialement prévu:
Soutenance de thèse de Christope
Papazian - ÉNS Lyon - Équipe MC2
Graphes d'automates finis : Reconnaissance & Calcul
En plaçant des automates finis sur des graphes finis quelconques, on obtient un modéle de calcul qui s'apparente aux automates cellulaires. Mais ici, les problèmatiques abordées dans cette thèse ne s'intéressent pas à la dynamique de ce système, mais plutôt à sa capacité propre à avoir conscience de lui-même. Ainsi, dans une première partie, j'aborde des problèmes de reconnaissance de propriétés géométriques, en m'intéressant aux plongements dans des graphes de Cayley, et dans une seconde partie, j'essaie de caractériser la puissance du modéle et ses particularités de calculabilité et j'établis des liens entre ce modèle de calcul et des classes de complexité classiques.
retour en haut de pageMardi 7 janvier 2003 à
13h30, Amphi B (au 3ème étage)
Alain
Denise - Professeur au LRI
- Équipe Bioinformatique
Séquences aléatoires et analyse des génomes
Un problème crucial dans l'analyse des génomes est de différencier, dans les séquences, les signaux ``biologiquement signifiants'' de ceux qui participent au bruit de fond. Pour ce faire, on compare les séquences biologiques à celles que l'on attendrait ``par hasard'' : à partir des différences mises en évidence, on peut inférer des propriétés purement biologiques. Plusieurs types d'approches existent, tant par des méthodes purement analytiques (à base de probabilités et de combinatoire) que par la simulation (génération de séquences aléatoires).
Je décrirai quelques-unes de ces approches.
Mardi 21 janvier 2003 à
13h30, Amphi B (au 3ème étage)
Christophe
Paul - CR CNRS au LIRMM - Équipe Algorithmique Combinatoire
Représentation implicites de graphes et petits graphes
universels
Coder un graphe en machine est un problème central de l'algorithmique. Peut-on imaginer des structures de données plus compactes et plus efficaces en terme de réponses aux requêtes que les classiques matrices d'adjacence et listes d'adjacence ? Un certain nombre de familles de graphes admettent des représentations implicites. Intuitivement si une telle famille de graphes possède 2^f(n) graphes différents à n sommets, la structure de données utilise O(f(n)) bits et permet de répondre en temps constant au test adjacence. Il faut noter qu'une telle représentation implique l'existence d'un graphe universel de taille polynomiale contenant tous les graphes à n sommets de la famille.
Nous avons étudié le problème plus général consistant à représenter les distances dans un graphe. Nous exhibons une famille non triviale en terme de nombre d'éléments pour laquelle le codage de la distance n'est guère plus gourmant en mémoire que le codage de l'adjacence. On en déduit l'existence d'une matrice universelle des distances pour cette famille. Il s'agit des graphes d'intervalles.
Mardi 11 février 2003 à
13h30, Amphi B (au 3ème étage)
Gil
Utard — CR INRIA (en détachement du LaRIA) — LIP —
Équipe ReMap
Pérennité dans les systèmes de stockage pair à pair
On constate aujourd'hui un très fort engouement pour les systèmes de fichiers pair à pair. On peut citer Napster, Freenet, Gnutella où les fichiers sont distribués sur l'ensemble des PCs. Ces systèmes sont des alternatives à l'approche client/serveur du WEB. En fait ces systèmes sont orientés essentiellement dans la mise en commun et dans la diffusion des données et des informations. Les objectifs avoués étant essentiellement celui de l'anonymat des sources d'informations, ce qui impose un surcoût non négligeable dans l'accès aux données. En général, il n'y a aucune garantie en ce qui concerne la fiabilité et la disponibilité des données.
Dans le même temps, d'autres systèmes moins populaires, car non dédié exclusivement à la diffusion de fichiers musicaux ou vidéos, ont été développés. On peut citer InterMemory, PAST ou Oceanstore. Ils ne se présentent plus non seulement comme étant des systèmes de partage de données, mais aussi comme des systèmes de partage d'espaces de stockage. À la différence des systèmes précédemment cités, ces nouveaux systèmes intègrent des mécanismes qui tente d'assurer la pérennité des données.
Après une présentation de différents systèmes, nous nous intéresserons aux mécanismes qui sont mises en oeuvre pour assurer la pérennité des données. Ces mécanismes sont basés sur la redondance. Nous présenterons une modélisation quantitative de l'efficacité de ces mécanismes sur la persistance des données, ainsi qu'une analyse de leurs coûts.
Mardi 4 mars 2003 à 13h30,
Amphi B (au 3ème étage)
Stéphan
Thomassé — Maître de conférence au LaPCS —
Université Claude Bernard Lyon 1
Stabilité et sous-graphe minimal fortement connexe
Mardi 1er avril 2003
à 13h30, Amphi B (au 3ème étage)
Éric
Gascard — ATER au LIFO — Université d'Orléans
Vérification formelle d'algorithmes parallèles
sur réseaux d'interconnexion symétriques
Cet exposé présentera une méthodologie de modélisation et de vérification d'algorithmes parallèles sur réseaux d'interconnexion symétriques. Nous utiliserons des techniques de preuve de théorèmes (theorem proving) et plus particulièrement la preuve par induction. Les preuves seront paramétrés sur le nombre de processeurs. La présentation se déroulera en quatre parties :
1) Modélisation formelle des réseaux symétriques dans un démonstrateur de théorèmes basé sur une logique du premier ordre + induction. Utilisation du formalisme des graphes de Cayley.
2) Modélisation et vérification fonctionnelle des primitives de communication collectives sur ces réseaux (broadcast, scatter, reduction, prefix-computation ....) : Définition des schémas des théorèmes permettant d'obtenir la correction fonctionnelle des primitives et déduction des invariants nécessaires aux preuves.
3) Modélisation et Vérification de programmes distribués : Utilisation d'une approche compositionnelle.
4) Exemples applicatifs sur l'hypercube :
-
Vérification formelle du calcul parallèle du produit matrice-vecteur
-
Vérification formelle du calcul parallèle du shape number d'une
image
Un des résultats principaux de ce travail est l'obtention automatique des invariants nécessaires aux preuves, ceci à partir de la notion de voisinage d'un processeur que nous avons formalisé.
Mardi 8 avril 2003 à 13h30, Amphi
B (au 3ème étage)
David Hough —
Sun Distinguished Engineer
IEEE 754R Status & Sun Microsystem Math Libraries
IEEE 754R Status. The IEEE 754R committee is slowly examining proposals for improving the IEEE 754 standard for binary floating-point arithmetic. Some proposals have been incorporated into a draft revision, such as standardizing quadruple precision and standardizing fused multiply-add. Many others proposals remain to be decided, such as incorporating decimal formats as well as binary, specifying alternate exception handling capabilities, requiring correctly-rounded conversion between internal binary formats and external decimal character formats, specifying max/min operations, etc...
Sun Microsystems Math Libraries. Sun Microsystems has developed several versions of the basic C <math.h> functions in libm. Each represents a different trade-off between accuracy, performance, generality, and portability of source code; the slowest, written in portable C code, provides 1/2 ulp rounding in all rounding modes,while the fastest for vector operations, which includes considerable SPARC assembly language, usually provides < 1 ulp rounding in the default rounding modes only.
Mardi 15 avril 2003 à
13h30, Amphi B (au 3ème étage)
Laurent
Théry — CR INRIA — Équipe Lemme — INRIA
Sophia Antipolis
Une visite guidée de la vérification formelle
avec l'outil de preuve Coq:
L'algorithme de Knuth pour les nombres premiers
Dans son livre "The Art of Computer Programming" Donald Knuth donne un algorithme pour calculer les n premiers nombres premiers. De façon assez surprenante, la vérification formelle de la correction d'un tel algorithme est loin d'être évidente et met en jeu un éventail assez large de techniques de vérification. Nous nous proposons de montrer comment la généricité et l'expressivité d'un outil de preuve comme Coq a rendu possible une telle vérification. L'exposé se voudra didactique et en particulier aucune connaissance préalable de Coq sera supposée.
Mardi 29 avril 2003 à 13h30,
Amphi B (au 3ème étage)
Clémence
Magnien — Étudiante en thèse au LIX — École
Polytechnique
Étude du modèle du tas
de sable :
points de vue algorithmique et algébrique
Le modèle du tas de sable abélien a été introduit en physique
par Bak, Tang et
Wiesenfeld comme un modèle type du phénomène de d'auto-organisation critique
(self-organized criticality). Plusieurs modèles proches ont ensuite été
introduits et étudés dans plusieurs disciplines, notamment en physique,
en sciences sociales et en informatique.
Il est connu que, pour ces modèles, l'ensemble des configurations atteignables à partir d'une configuration initiale donnée peut être ordonné naturellement comme un treillis (ensemble ordonné particulier). Nous presenterons une étude de la structure de cet ensemble pour un modèle particulier, le Chip Firing Game (CFG), qui joue un rôle central parmi ces modeles. Cette etude permet de mieux comprendre pourquoi la structure de treillis apparaît fréquemment dans ce contexte. D'autre part, un ensemble de configuration particulières du modèle du tas de sable abélien, appelées recurrentes, a la propriété de former un groupe pour l'addition. Nous presentérons certaines configurations remarquables pour leur structure auto-similaire, et nous presenterons des axes d'étude qui permettent de comprendre cette structure.
Mardi 13 mai 2003 à 13h30,
Amphi B (au 3ème étage)
Nadia
CREIGNOU — Professeur au LIF — Équipe Logique et
Complexité
Un théorème de classification croisée,
complexité versus transition de phase, pour les problèmes de
satisfaction
de contraintes booléennes
Un phénomène de transition de phase brusque a été mis en évidence il y a quelques années pour le problème NP-complet bien connu 3-SAT. De nature probabiliste ce phénomène se traduit par le fait que la probabilité qu'une formule 3-CNF aléatoire soit satisfaisable présente un brusque changement quand le ratio du nombre de clauses sur L sur le nombre de variables n varie. Plus précisément il existe une valeur critique c telle que si L/n<c alors la formule aléatoire est presque surement satisfaisable, alors que si L/n>c elle est presque surement insatisfaisable. Ce comportement probabiliste a suscité beaucoup d'intérêt ces dernières années car il a été observé d'un point de vue pratique que les instances difficiles des problèmes NP-complets coincidaient avec la fenêtre de transition.
Nous établissons un théorème de classification croisée, complexité (P ou NP-complet) versus nature de la transition de phase (brusque ou progressive), pour les problèmes de satisfaction de contraintes booléennes. Nous proposons un critère concis et local qui, étant donné un ensemble de types de contraintes autorisées en entrée, permet de décider facilement si le problème de satisfaisabilité associé a une transition de phase brusque ou progressive. De plus notre étude fournit une première preuve uniforme, et donc instructive, du fait que de nombreux problèmes de satisfaisabilité bien connus tels k-SAT, k-XOR-SAT, Non-Tous-Egaux-k-SAT, 1-parmi-k-SAT, ont une phase de transition brusque.
Mardi 27 mai 2003 à 13h30,
Amphi B (au 3ème étage)
Arnaud
Tisserand — CR INRIA au LIP — Équipe Arenaire
DSP : des processeurs dédiés pour le traitement numérique
du signal
Transparents de la
présentation
Les DSP (Digital Signal Processors) sont des processeurs dédiés aux applications de traitement du signal. Les besoins et les contraintes de ces applications nécessitent des processeurs avec des architectures et des jeux d'instructions parfois différents de ceux des processeurs généralistes. Le but de cet exposé est une petite présentation des principales caractéristiques de ces processeurs. En particulier, nous regarderons leur architecture interne au niveau du pipeline, des accès mémoires et des différentes unités fonctionnelles. Nous nous appuierons sur la description de quelques processeurs typiques et des applications associées. Enfin, nous essayerons de comparer leur évolution avec celle des processeurs généralistes.
Mardi 10 juin 2003 à 13h30, Amphi B (au 3ème étage)
Patricia
Bouyer — CR CNRS au LSV — ÉNS Cachan
Untameable Timed Automata!
Le modèle des automates temporisés est un modèle très répandu et étudié. Depuis maintenant 8 ans, des outils implantant ce modèle sont disponibles et ont été utilisés avec succès pour vérifier de vrais systèmes. Cependant, j'ai récemment montré qu'une des techniques utilisées pour vérifier les automates temporisés, l'analyse en avant, n'est pas correcte d'un point de vue algorithmique : en effet, il existe des automates temporisés pour lesquels le résultat de l'algorithme appliqué à ces automates est erroné. Je vais donc présenter ce résultat et expliquer quels sont précisément les problèmes.
Voici un lien vers le bug en question: http://www.lsv.ens-cachan.fr/~bouyer/bug.php
Mardi 24 juin 2003 à 13h30,
Amphi B (au 3ème étage)
Pham CongDuc — MdC au LIP — Équipe
RESO — Université Lyon
I
Multicast technology: what it is, what have been done, what's next?
Le multicast IP est une technologie qui vise a fournir un support de diffusion efficace et résistant au facteur d'echelle dans l'Internet. Ce n'est pas une technologie nouvelle, mais elle est en constante evolution et presente un grand nombre de defis. Meme si un grand nombre de personnes ont entendu parle du multicast, peu connaissent reellement les techniques qu'il y a derriere ce mot. Les nombreux protocoles, les multiples interactions entre les couches de communication et l'evolution constante des propositions contribuent fortement a ce flou. Ce seminaire tente de presenter de maniere claire et structuree ce qu'est le multicast a l'audience la plus large possible. Apres avoir presente les techniques de base du multicast au niveau du routage et du transport, ce seminaire poursuivra en presentant les points durs qui existent actuellement, qui ne sont pas necessairement d'ordre technique. Des applications du multicast dans un grand nombre de domaine, incluant la grille de calcul seront presentees pour concretiser apres de l'auditeur la maniere dont le multicast peut devenir indispensable sur l'Internet.
REPORTÉ
Julien
Barral — CR INRIA - Projet Fractales
Analyse multifractale d'une version simplifiée de
TCP
À suivre...
Dernière mise à jour: mercredi, 9 juillet, 2003 9:14 .