- Annonce

[Annonce] [Séminaire LRDE] : mercredi 7 juin 2006
by Daniela Becker 02 Jun '06

02 Jun '06

Bonjour, Vous êtes tous cordialement invités à assister au séminaire qui aura lieu le mercredi 7 juin à 14 heures en amphi P01 (KB). ----------------------------------------------------------------------- Le programme : *BDD, ALGORITHMES GENETIQUES & MARKOV* http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-06-07 BDD 14h00 : BDD distribués et Java -- Guillaume Guirado 14h30 : Répartition des DDD en Erlang -- Samuel Charron ALGORITHMES GENETIQUES 15h00 : Programmation génétique & Corewar -- Jérémy Marc MARKOV 15h45 : Vérification du locuteur -- Charles-Alban Deledalle 16h15 : Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester 16h45 : Chaînes de Markov continues en présence d'incertitudes -- Nicolas Neri ----------------------------------------------------------------------- Les Résumés des exposés : ************************* BDD * BDD distribués et Java -- Guillaume Guirado Les BDD (Diagrammes de Décision Binaires) ont été très largement étudiés depuis leur introduction à la fin des années 80. De très nombreuses implémentations ont d'ailleurs été proposées. Cependant, rares sont les bibliothèques permettant de distribuer notre diagramme sur un cluster. Partant de ce constat, l'implémentation, dans un langage moderne, d'une bibliothèque de gestion de BDD permettant la répartition sur un grand nombre de machines est nécessaire. Cela permettra d'augmenter considérablement la mémoire disponible, et donc de résoudre des problèmes plus complexes. Pour cela, nous avons choisi le langage Java. Durant la présentation, nous verrons les principales propriétés des BDD et leurs opérations. Ensuite, nous analyserons les résultats d'une implémentation non répartie, avant de finalement exposer les choix, forces et faiblesses, de notre bibliothèque répartie. * Répartition des DDD en Erlang -- Samuel Charron Les DDD (Data Decision Diagrams) généralisent le concept de BDD, en permettant de ne pas se limiter aux fonctions booléennes. Cependant, ils n'apportent pas de solution supplémentaire au problème de mémoire. La répartition de BDD a déjà été longuement étudiée sans donner de résultat réellement satisfaisant. Une étude sur les propriétés des DDD nous a permis de réaliser la répartition. Nous utilisons pour cela Erlang, un langage intégrant des primitives de communications et de parallélisation Lors de ce séminaire, nous vous présenterons les DDD. Ensuite, une introduction à Erlang et a l'implémentation réalisée sera effectuée. Enfin, nous comparerons plusieurs algorithmes de répartition existants sur les BDD en y ajoutant d'autres algorithmes nouveaux. ALGORITHMES GENETIQUES * Programmation génétique & Corewar -- Jérémy Marc Les algorithmes génétiques existent depuis les années 80 et constituent une catégorie à part dans l'algorithmique évolutionnaire. Directement inspirés de la nature, ou plus exactement de la biologie, ils ont pour but d'approcher les solutions optimales en faisant varier les paramètres caractéristiques des individus. Lorsque ces individus sont des programmes, qui plus est en assembleur de type Corewar, la tâche devient nettement plus ardue. En effet il devient complexe d'exhiber ces paramètres et difficile de les modifier sans risquer d'altérer considérablement la cohérence de l'individu. Nous présenterons certaines de ces problématiques, puis proposerons plusieurs solutions que nous comparerons et expliquerons. MARKOV * Vérification du locuteur -- Charles-Alban Deledalle La vérification du locuteur consiste à détecter si un segment de parole est réellement prononcé par un individu présumé. Cela est mis en opposition à l'identification dont le but est de reconnaître l'auteur du message. Au cours de ce séminaire nous examinerons trois approches. La première approche, probabiliste (état de l'art), utilise les modèles de mixture gaussienne. Puis nous proposerons deux solutions basées sur les méthodes SVM. La différence entre ces deux dernières se situe au niveau des noyaux et des caractéristiques utilisés. Notre travail s'inscrit dans le prolongement de l'évaluation NIST, et dans le cadre de l'évaluation ISCSLP en cours. * Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester Le model-checking consiste à vérifier certaines propriétés sur un modèle donné. Il existe plusieurs méthodes pour résoudre ce problème, dont une méthode approchée, permettant de réduire le temps de calcul. Cette méthode est quantitative : ce qui nous intéresse est la probabilité que la formule soit vraie. Mais il y a des cas où le qualitatif est suffisant : ce qui nous intéresse est de savoir si cette probabilité est supérieure ou inférieure à un certain seuil. Nous présenterons d'abord le model-checking, et l'algorithme implémenté dans APMC, puis une optimisation de celui-ci dans le cas de la vérification qualitative de propriétés. Nous finirons par des tests, théoriques et expérimentaux. * Chaînes de Markov continues en présence d'incertitudes -- Nicolas Neri Le 26 Mars 2006 lors de la 12e conférence internationale TACAS, Khoushik SEN et al. ont présenté un article sur la vérification de programmes en utilisant les chaînes de Markov finies à temps discret pour lesquelles la probabilité exacte des transitions n'est pas connue. Ce séminaire présentera les travaux en cours sur l'extension de l'algorithme de Khoushik SEN et al. pour les chaînes de Markov à temps continu présentant des incertitudes. Le but sera de trouver un ensemble de variables satisfaisant certaines contraintes et de vérifier la faisabilité de celles-ci grâce à la résolution des BMIs. -- Daniela Becker

1 0

[Annonce] [Séminaire LRDE] : mercredi 24 mai 2006
by Daniela Becker 23 May '06

23 May '06

Bonjour, Nous sommes heureux de vous annoncer le deuxième de la série des séminaires du LRDE de mai-juin 2006. Vous êtes tous cordialement invités à assister au séminaire qui aura lieu demain, mercredi 24 mai à 14 heures en amphi P004 (KB). ----------------------------------------------------------------------- Le programme : *MARKOV, OLENA & VAUCANSON* http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-05-24 MARKOV 14h00 : Classement de pages Web -- Johan Oudinet OLENA 14h30 : Taxonomie des images dans Olena -- Christophe Berger 15h00 : Segmentation temps réel -- Nicolas Widynski VAUCANSON 15h45 : Automates et performance -- Guillaume Lazzara 16h15 : Synchronisation des transducteurs -- Guillaume Leroi 16h45 : Fermeture d’un automate -- Matthieu Varin ----------------------------------------------------------------------- Les Résumés des exposés : ************************* MARKOV * Classement de pages Web -- Johan Oudinet Les moteurs de recherche ordonnent les pages de leur index pour répondre rapidement et efficacement aux requêtes des internautes. Le critère pour établir cet ordre doit être indépendant de la requête et il doit refléter la "popularité" de chaque page. Cette notion abstraite de "popularité" est appliquée par des algorithmes qui se basent sur la structure de l'index. Le "PageRank" est le plus connu et le plus utilisé. Après avoir présenté le fonctionnement du "PageRank", nous décrirons des algorithmes plus rapides et peut-être même plus pertinents que le "PageRank". OLENA * Taxonomie des images dans Olena -- Christophe Berger Olena est une bibliothèque générique de traitement d'images. Il est important qu'elle puisse offrir à ses utilisateurs tous les outils nécessaires à leurs besoins. Ceci se traduit par une réflexion sur la modélisation de la bibliothèque au regard des types d'images qu'elle doit supporter. Nous allons présenter les types d'images élémentaires que nous souhaitons intégrer à Olena ainsi que les types, appelés "morpheurs", qui nous permettent d'étendre la gamme des types d'images. Nous caractériserons les propriétés des différents types d'images et nous proposerons une modélisation à l'aide du paradigme SCOOP 2. Finalement nous présenterons l'intégration de ce travail dans Olena. * Segmentation temps réel -- Nicolas Widynski En traitement d'images, la segmentation a pour but de partitionner l'image en plusieurs régions, selon des critères de sélection. Le but est généralement d'extraire des objets caractéristiques de l'image en vue d'effectuer un traitement particulier sur ces régions, ou tout simplement de simplifier l'image. Bien souvent, les méthodes d'extraction nécessitent un à priori sur certaines caractéristiques des objets, et ne sont donc pas génériques. Le domaine d'application est vaste : médical (extraction de tumeur, segmentation du cerveau,...), reconnaissance humaine (main, iris,...), suivi d'objets (bien souvent de personnes). Dans la littérature, il existe beaucoup de méthodes dévouées à la segmentation d'images. Quelques-unes fonctionnent en un temps réel, dédiées le plus souvent au suivi d'objets dans les séquences d'images. Nous proposons de comparer plusieurs méthodes de segmentation temps réel. Nous étudierons tout d'abord des algorithmes classiques (watershed, watersnake, snake) que nous opposerons à une seconde approche, tout à fait différente, basée sur les opérateurs connectés. VAUCANSON * Automates et performance -- Guillaume Lazzara Passer d’une théorie mathématique à une implémentation sur machine n’est pas toujours évident. Bien souvent d’ailleurs, l’implémentation la plus intuitive n’est pas la plus performante. Les automates n’échappent pas à cette règle. Étant capable de pousser les machines au-delà de leurs limites, optimiser leur implémentation et les algorithmes associés est une réelle nécessité. C’est donc dans cet esprit que nous vous présenterons les problèmes de performances liés aux automates booléens, ainsi qu’une étude des méthodes les plus pertinentes qui pourraient être utilisées à l’avenir dans Vaucanson. * Synchronisation des transducteurs -- Guillaume Leroi Un transducteur est un automate qui pour une entrée reconnue donne une certaine sortie. On peut voir ces objets comme des automates dont les transitions au lieu d'ëtre étiquetées par une lettre sont étiquetées par un couple de lettres, voir un couple de mots. Ces transducteurs peuvent représenter des relations par exemple. Le but de la synchronisation est de ramener des transducteurs étiquetés par des mots à des transducteurs étiquetés par des lettres dans le but de pouvoir calculer des intersections de relations, ou bien déterminiser le transducteur en considérant les couples de lettres comme des lettres d'un autre alphabet. Nous présenterons deux algorithmes; l'un permettant de déterminer si un transducteur est synchronisable, et l'autre de synchroniser un transducteur. * Fermeture d’un automate -- Matthieu Varin Les transitions spontanées sont très utiles dans le cadre de la manipulation d'automates. Cependant, il arrive bien souvent que l'on ait besoin de les supprimer. On peut citer les cas de la déterminisation d'automates, l'évaluation dans Z, ... La suppression des transitions spontanées s'appelle la fermeture de l'automate. Il existe deux types de fermeture : avant et arrière. Une implémentation de la fermeture existe déjà dans Vaucanson. Cette implémentation est basée sur la méthode décrite par Jacques SAKAROVITCH dans son livre 'Éléments de théorie des automates' (pages 87 - 88). C'est une variante optimisée qui est proposée pour ce séminaire. Celle-ci pose des problèmes dans le cas d'automates sur Z que nous allons aborder. -- Daniela Becker Responsable administrative du LRDE

1 0

[Annonce] L'air de rien 4
by Roland Levillain 10 May '06

10 May '06

Le quatrième numéro du bulletin du LRDE est sorti. Il est disponible ici : http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/200605-l-air-de-ri… -- Roland Levillain

1 0

[Annonce] [Séminaire LRDE] : mercredi 17 mai 2006
by Daniela Becker 09 May '06

09 May '06

Bonjour, Vous êtes tous cordialement invités à assister au séminaire du LRDE qui aura lieu le mercredi 17 mai à 14 heures en amphi P004 (KB). ----------------------------------------------------------------------- Le programme : *VAUCANSON & TRANSFORMERS* http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-05-17 VAUCANSON 14h00 : Remodélisation du projet Vaucanson -- Robert Bigaignon 14h30 : On m'a dit que 275 604 541 était premier -- Michael Cadilhac 15h00 : Extension du format XML -- Florent Terrones TRANSFORMERS 15h45 : Preprocessing & Unpreprocessing du C et C++ -- Thomas Largillier 16h15 : Grammaires hors-contexte et désambiguïsation -- Renaud Durlin 16h45 : Vectorisation automatique grâce à la transformation de programme -- Alexandre Borghi ----------------------------------------------------------------------- Les Résumés des exposés : ************************* VAUCANSON * Remodélisation du projet Vaucanson -- Robert Bigaignon Vaucanson est une bibliothèque générique de manipulation d'automates finis conçue en 2001. Son but est de permettre la manipulation efficace de n'importe quel type d'automate tout en restant fidèle au cadre algébrique établi par la théorie des automates. Ceci au prix d'une écriture parfois lourde et souvent difficile. Aujourd'hui, nous envisageons la refonte du coeur de la bibliothèque afin de tirer parti des dernières avancées notamment en termes de programmation C++. Ainsi, nous présenterons lors de cet exposé une comparaison de techniques de modélisations appliquées à un sous-ensemble représentatif de Vaucanson. * On m'a dit que 275 604 541 était premier -- Michael Cadilhac Quand sont évoqués conjointement l'arithmétique et la cryptographie, un des premiers points communs qui vient à l'esprit se trouve dans la propriété de primalité des nombres. La méthode la plus simple pour tester si un nombre est premier est de reprendre la définition, c'est-à-dire lister les diviseurs de ce nombre et vérifier qu'il y en a exactement 2. Mais cet algorithme naïf est extrêmement coûteux, il s'agira donc non pas de passer par la définition, mais par les propriétés des nombres premiers. Nous présenterons un large éventail d'algorithmes de test de primalité, qu'ils soient probabilistes ou déterministes, chacun a son domaine d'utilisation. Nous étudierons des tests rapides pour petits nombres, ou pour nombres probablement premiers, aussi bien que des algorithmes généraux dont, en particulier, celui montrant que le test de primalité est dans la classe de complexité P. * Extension du format XML -- Florent Terrones Proposé lors des différentes conférences CIAA (Conference on Implementation and Application of Automata), le format XML de description d'automates présenté par l'équipe Vaucanson a pour but de permettre et faciliter le transfert des informations d'un automate entre les différents logiciels qui les manipulent. On peut en effet charger en mémoire un automate stocké dans un fichier XML et le modifier dans Vaucanson, ou au contraire sauvegarder un automate en format XML. Mais un détail gêne encore la parfaite portabilité de ce format: les étiquettes des transitions sont pour l'instant de simples chaînes de caractères. Elles sont donc dépendantes des syntaxes utilisées par chaque logiciel, à l'instar de Vaucanson. Le but de ce séminaire est de faire le point sur les propriétés que cette extension doit satisfaire, puis d'écrire cette dernière. Enfin, certaines parties du contenu de Vaucanson seront modifiées afin de supporter ces changements. TRANSFORMERS * Preprocessing & Unpreprocessing du C et C++ -- Thomas Largillier L'objectif du projet Transformers est de fournir des transformations de source à source pour les langages C et C++. Ces transformations se doivent d'être les plus fidèles possibles. Les directives de compilation sont omniprésentes dans des sources C/C++. L'utilisateur souhaite naturellement les retrouver après avoir transformé son fichier source. Il est donc impossible d'utiliser les outils libres existants puisque ceux-ci ne font le travail que dans un seul sens. Après un exposé des problèmes rencontrés dans une telle démarche, il vous sera présenté une implémentation réalisée, dans le cadre du projet Transformers, avec les outils de Stratego/XT. * Grammaires hors-contexte et désambiguïsation -- Renaud Durlin Les grammaires hors-contexte sont de plus en plus utilisées car elles permettent d'analyser des langages réels en utilisant un formalisme simple et naturel. De manière générale, les grammaires hors-contexte permettent de spécifier des langages ambigus. En utilisant de telles grammaires, un analyseur syntaxique généralisé produit non pas un arbre mais une forêt de parse. La désambiguïsation consiste alors à analyser cette forêt pour obtenir l'unique arbre correspondant à l'entrée en prenant en considération les règles sémantiques contextuelles. Nous verrons trois méthodes pour effectuer la désambiguïsation : la réécriture de termes guidée par des spécifications algébriques (ASF+SDF), l'utilisation de stratégies (Stratego/XT) et le formalisme des grammaires attribuées (Transformers). Nous discuterons des points forts et des points faibles de chacune de ces approches. * Vectorisation automatique grâce à la transformation de programme -- Alexandre Borghi La majorité des processeurs sur le marché permet de tirer parti de la vectorisation. Cependant, les langages et le code existants n'y sont pas particulièrement adaptés. Les derniers compilateurs essaient d'auto-vectoriser mais les résultats sont rarement satisfaisants. Le C étant intrinsèquement séquentiel, il exprime un grand nombre de dépendances qui n'ont pas lieu d'être. Ceci rend difficile la vectorisation automatique. Les outils d'auto-vectorisation doivent en particulier considérer les boucles pour en extraire un maximum d'information suivant des analyses de dépendances parfois très élaborées. Il s'agit ici de transformer un fichier source C afin de le rendre plus facilement vectorisable par les derniers compilateurs à l'aide de Transformers et des outils de transformation de programmes qu'il fournit. -- Daniela Becker Responsable administrative du LRDE

1 0

[Annonce] L'air de rien 3
by Daniela Becker 13 Apr '06

13 Apr '06

Le troisième numéro du bulletin du LRDE est sorti. Il est disponible sur: http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/200604-l-air-de-ri… -- Daniela Becker

1 0

[Annonce] [comp.text.tex] CTAN package update: FiXme version 3.2
by Didier Verna 12 Apr '06

12 Apr '06

-- Didier Verna, didier(a)lrde.epita.fr, http://www.lrde.epita.fr/~didier EPITA / LRDE, 14-16 rue Voltaire Tel.+33 (1) 44 08 01 85 94276 Le Kremlin-Bicêtre, France Fax.+33 (1) 53 14 59 22 didier(a)xemacs.org

1 0

[Annonce] L'air de rien 2
by Daniela Becker 08 Mar '06

08 Mar '06

Le deuxième numéro du bulletin du LRDE est sorti. Il est disponible sur: http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/200603-l-air-de-ri… -- Daniela Becker

1 0

[Annonce] L'air de rien
by Daniela Becker 08 Dec '05

08 Dec '05

Jouez hautbois, résonnez musette; Chantons tous son avènement: Il est né le ... bulletin du labo :) Vous pouvez l'admirer en couleur sur http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/200512-l-air-de-ri… -- Daniela

1 0

[Annonce] ACM TOCL
by Sylvain Peyronnet 22 Nov '05

22 Nov '05

J'avais oublié de dire que la publi journal suivante a été accepté : Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet and Michel de Rougemont. Probabilistic abstraction for model checking: An approach based on property testing. accepted to ACM TOCL. Voili voilo S.

1 0

[Annonce] Publi RIVF'06
by Akim Demaille 22 Nov '05

22 Nov '05

Thomas, Sylvain et Akim sont heureux de vous faire part de l'acceptation de leur article à RIVF 2006. Probabilistic Verification of Sensor Networks https://publications.lrde.epita.fr/2006-02-rivf Sensor networks are networks consisting of miniature and low-cost systems with limited computation power and energy. Thanks to the low cost of the devices, one can spread a huge number of sensors into a given area to monitor, for example, physical change of the environment. Typical applications are in defense, environment, and design of ad-hoc networks areas. In this paper, we address the problem of verifying the correctness of such networks through a case study. We modelize a simple sensor network whose aim is to detect the apparition of an event in a bounded area (such as a fire in a forest). The behaviour of the network is probabilistic, so we use APMC, a tool that allows to approximately check the correctness of extremely large probabilistic systems, to verify it. @InProceedings{ demaille.06.rivf, author = {Akim Demaille and Sylvain Peyronnet and Thomas Hérault}, title = {Probabilistic Verification of Sensor Networks}, booktitle = {Proceedings of the Fourth IEEE International Conference on Computer Sciences, Research, Innovation and Vision for the Future (RIVF)}, year = {2006}, address = {Ho {C}hi {M}inh City, {V}ietnam}, month = {February}, project = {APMC}, }

2 2