Bonjour, nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE. Il aura lieu le mercredi 19 janvier 2011 à 14 heures en Amphi 4 (KB). ------------------------------------------------------------------ Au programme: *OLENA, VAUCANSON, CLIMB et SPOT* http://publis.lrde.epita.fr/Seminar-2011-01-19 OLENA *14h00 : Un algorithme rapide pour l’arbre auto-dual -- Edwin Carlinet VAUCANSON *14h30 : Mécanique de Vaucanson 2.0 -- Alex Hamelin CLIMB *15h15 : Concevoir l’interface d’une bibliothèque générique en Common Lisp -- Loïc Denuzière SPOT *15h45 : Model Checking LTL utilisant des automates Testeurs -- Ala-Eddine Ben-Salem ----------------------------------------------------------------------- Les Résumés des exposés : ************************** OLENA - TRAITEMENT D’IMAGES GÉNÉRIQUE ET PERFORMANT 14h00 : Un algorithme rapide pour l’arbre auto-dual -- Edwin Carlinet Ces dernières années, les opérateurs connectés ont gagné une certaine popularité dans le domaine du traitement d’images, ils ont en effet été largement utilisés dans le cadre de filtrage, de segmentation, de détection d’objets. . . Néanmoins, plusieurs défauts ont été mis en évidence, le plus important étant la dépendance au contraste, on ne peut que détecter soit les objets clairs, soit les objets foncés. Les opérateurs auto-duaux permettent d’opérer sur les objets clairs et foncés à la fois et ne souffrent donc pas du défaut des opérateurs connectés classiques. En revanche, les opérateurs auto-duaux sont plus difficiles à mettre en place et les algorithmes actuellement disponibles sont coûteux en temps de calcul. Nous proposons un nouvel algorithme pour calculer les opérateurs auto-duaux basés sur l’union-find de Tarjan ; celui-ci offrant de meilleures performances que l’algorithme d’arbres de contours à l’état de l’art. VAUCANSON - BIBLIOTHÈQUE DE MANIPULATION D’AUTOMATES 14h30 : Mécanique de Vaucanson 2.0 -- Alex Hamelin Vaucanson est une plateforme de manipulation d’automates finis et de transducteurs dont l’interface s’est montrée trop complexe. Pendant les deux dernières années, des travaux ont été entrepris afin d’introduire le concept de kind d’un automate dans la bibliothèque. Afin d’y arriver, l’interface fut refaite ainsi que la mécanique interne de Vaucanson. Ceci amena plusieurs changements dans les structures de données, les algorithmes et la définition de l’interface. Nous exposerons ces modifications tout en mettant en avant les divers pièges qu’un développeur pourrait rencontrer en travaillant dans le coeur de la bibliothèque. Ce travail pourra amener à des mesures de performances entre Vaucanson 2.0 et la dernière version stable de la bibliothèque. CLIMB - TRAITEMENT D’IMAGES EN LISP 15h15 : Concevoir l’interface d’une bibliothèque générique en Common Lisp -- Loïc Denuzière Climb est une bibliothèque de traitement d’images générique. Elle est implémentée en Common Lisp et vise un dynamisme et une facilité d’utilisation maximaux. Dans ce but, l’interface utilisateur doit être à la fois suffisamment puissante pour ne pas cacher certaines fonctionnalités de la bibliothèque sous-jacente, et intuitive pour l’utilisateur. La difficulté est de créer une interface faisant un minimum de compromis entre ces caractéristiques, tout en restant suffisamment extensible pour les garder quand la bibliothèque évolue. Après quelques rappels sur le design générique de Climb, nous présentons les modifications que nous avons apportées à l’interface existante pour améliorer son utilisabilité sans restreindre ses capacités. SPOT - BIBLIOTHEQUE DE MODEL CHECKING 15h45 : : Model Checking LTL utilisant des automates Testeurs -- Ala-Eddine Ben-Salem Spot est une bibliothèque C++ de model checking basée sur l'approche automate, et utilisant des automates de Büchi. Le problème principal de cette approche est l’explosion de l’espace d’états à explorer. Afin de réduire la taille des automates représentant l’espace d’états, nous avons implémenté dans Spot une solution qui utilise des automates Testeurs à la place des automates de Büchi. Nous présenterons les différentes étapes de construction d'un automate Testeur à partir d'un automate de Büchi. Ensuite, nous détaillerons les algorithmes de vérification manipulant des automates Testeurs. ------------------------------------------------------------------- Daniela Becker