Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mardi 3 juillet 2018 à partir de 10h00 en Amphi 4 (KB). Les étudiants ING1 et ING2 présenteront le résultat de leurs travaux des derniers mois. Au programme : SPOT — BIBLIOTHEQUE DE MODEL CHECKING 10h00 Recherche de chemin acceptant bi-bande dans Spot – CLÉMENT GILLARD Nous proposons un algorithme de recherche de chemin acceptant bi-bande, qui vient compléter le test de vacuité bibande présenté l’an dernier, et nous permet de l’utiliser dans des applications plus concrètes. 10h30 Création d’une bibliothèque d’antichaîne – ARTHUR REMAUD Une antichaîne est un sous-ensemble d’éléments tous deux à deux incomparables. Les antichaînes sont utilisées dans la théorie des automates comme structures de données pour stocker des ensembles d’états. De nouveaux algorithmes ont été implémentés et évalués afin d’optimiser l’insertion dans une antichaîne. 11h00 Implémentation des transitions invisibles et transparentes dans Spot – VINCENT TOURNEUR Dans le domaine de la vérification formelle, la Réduction d’Ordre Partiel (ROP) est une méthode qui permet de réduire notablement la taille des structures de données utilisées pour représenter les différentes exécutions d’un programme. Pour vérifier des formules LTL en utilisant la ROP, il faut ajouter des vérifications supplémentaires pour ne pas omettre des exécutions qui modifient les valeurs des propositions atomiques de la formule. Nous expliquons le fonctionnement de deux méthodes qui résolvent ce problème et leurs implémentations dans Spot : les méthodes des transitions invisibles et transparentes. CLIMB — TRAITEMENT D’IMAGES EN LISP 13h30 SUBTYPEP : une implémentation de l’algorithme de Baker – LEO VALAIS SUBTYPEP est un prédicat du langage Common Lisp qui indique si un type est un sous-type d’un autre. Étant donné le système de typage du langage, il n’est pas toujours possible de donner de réponse. Les implémentations de cette fonction ayant souvent tendance à ne pas répondre, même lorsque c’est possible, Baker a publié un algorithme qu’il prétend plus efficace. Nous proposons ici une implémentation partielle de son algorithme et présentons ses avantages et ses inconvénients. OLENA — TRAITEMENT D’IMAGES GÉNÉRIQUE ET PERFORMANT 14h00 Optimisation d’une bibliothèque de traitement d’images – VIRGILE HIRTZ La bibliothèque de traitement d’images Pylene n’est pas conforme aux nouveaux standards et subit des pertes de performance. Nous présentons un nouveau design résolvant ces problèmes. 14h30 Intégration d’histogrammes dans l’algorithme NL-Mean pour le débruitage d’images – ALIONA DANGLA L’objectif principal de ce projet est d’incorporer l’information liée à la distribution statistique des couleurs grâce à l’utilisation d’histogrammes dans NL-Mean. Cela permet d’effectuer toute transformation qui n’affecte pas la forme des histogrammes et ajouter des régions qui auraient pu ne pas être prises en compte dans l’algorithme originel. 15h00 Segmentation automatique du coeur – YOUNES KHOUDLI Nous proposons ici une méthode de segmentation automatique, adaptée d’une méthode développée pour la segmentation du cerveau humain. -- Daniela Becker Responsable administrative du LRDE