Bonjour, nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE. Il aura lieu demain, mercredi 6 janvier 2010 à 14 heures en Amphi Masters (KB). ----------------------------------------------------------------------- Au programme: *Vaucanson, Spot, Transformers et Compilateur Tiger* https://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2010-01-06 VAUCANSON * 14h00 : Adapter les structures de données de Vaucanson au concept de kind et à une interface rénovée -- Jérôme Galtier * 14h30 : Adaptation d’algorithmes de Vaucanson à une interface plus simple – Florent d'Halluin SPOT * 15h00 : Nouvelle traduction de LTL en TGBA dans Spot –- Damien Lefortier * 15h30 : La complémentation d’automates de Büchi à travers des automates alternants –- Guillaume Sadegh TRANSFORMERS * 16h15 : Étude et analyse de l’écriture d’extensions du C++ grâce à Transformers –- Vincent Ordy COMPILATEUR TIGER * 16h45 : Intégration de techniques de parallélisation dans le compilateur Tiger –- Warren Seine ----------------------------------------------------------------------- Les Résumés des exposés : ************************** VAUCANSON * 14h00 : Adapter les structures de données de Vaucanson au concept de kind et à une interface rénovée –- Jérôme Galtier La conception des automates dans Vaucanson occupe une place centrale concernant la généricité de la bibliothèque. Nous voulons pouvoir étendre cette modélisation pour supporter de nouveaux types et spécialiser des comportements afin d’améliorer les performances. L’introduction récente du concept de kind à la bibliothèque ainsi que la définition d’une nouvelle interface des automates ont pour objectif de rationaliser les structures de données déjà présentes dans Vaucanson, comme les graphes utilisant Boost Multi Index. Le kind d’un automate est le type d’étiquettes qu’il porte sur ses transitions, une lettre ou un mot par exemple. L’utilisateur peut alors, à travers une hiérarchie d’itérateurs respectant la nouvelle interface, itérer de manière efficace sur les transitions portant une occurrence de ce kind spécifié comme prédicat (itérer sur les transitions portant la lettre a par exemple). Le gain est visible car l’utilisateur était contraint d’itérer sur le support d’un polynôme avant ces améliorations. * 14h30 : Adaptation d’algorithmes de Vaucanson à une interface plus simple –- Florent d'Halluin Vaucanson est une bibliothèque C++ de manipulation d’automates finis. Le feedback utilisateur montre que Vaucanson est lent et que l’interface de la bibliothèque qui permet de manipuler les automates directement est complexe. Pour améliorer Vaucanson, l’équipe de développement met en place une interface simplifiée sur la structure de données Automata et réinstaure une modélisation saine de l’implémentation sous-jacente. Une conséquence de ces changements est que les algorithmes disponibles dans Vaucanson doivent être adaptés à la nouvelle interface. L’adaptation de ces algorithmes donne l’opportunité d’étudier l’impact des changements récents sur les performances et l’accessibilité de Vaucanson. Grâce à la simplicité de la nouvelle interface, les optimisations possibles deviennent plus visibles. SPOT * 15h00 : Nouvelle traduction de LTL en TGBA dans Spot –- Damien Lefortier Spot est une bibliothèque de model checking centrée sur l’approche automate et qui permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur des modèles représentés par des automates de Büchi généralisés basés sur les transitions (TGBA). Spot propose actuellement trois algorithmes pour traduire des formules LTL en TGBA, une des étapes principales de l’approche automate. Nous présentons une quatrième traduction, introduite par Tauriainen, qui utilise des automates alternants basés sur les transitions (TAA) comme représentation intermédiaire. Nous le comparerons ensuite aux trois algorithmes déjà présents dans Spot. * 15h30 : La complémentation d’automates de Büchi à travers des automates alternants –- Guillaume Sadegh Le model checking est un domaine de la vérification formelle, qui permet de vérifier le comportement d’un système avec l’aide de formules logiques temporelles. Spot est une bibliothèque de model checking qui repose sur une des techniques du domaine : l’approche automate. Dans cette approche du model checking, le système et les formules sont représentés sous forme d’automates acceptant des mots de longueur infinie, et plus particulièrement des automates de Büchi. Spot propose de nombreux algorithmes aux utilisateurs de la bibliothèque pour manipuler ce type d’automates, en vue d’applications au model checking. Une opération sur ces automates a récemment été ajoutée dans Spot : la complémentation. La recherche d’algorithmes effectuant cette opération est toujours d’actualité puisqu’il n’existe toujours pas d’algorithme atteignant les bornes théoriques optimales. Nous présenterons deux algorithmes récents de complémentation que nous venons d’ajouter dans Spot, qui se basent sur des automates alternants. TRANSFORMERS * 16h15 : Étude et analyse de l’écriture d’extensions du C++ grâce à Transformers –- Vincent Ordy Le projet Transformers permet de faire de la transformation source à source pour les languages C et C++. Le but est de pouvoir effectuer une analyse syntaxique d’un langage d’entrée, du C ou C++ étendu pour accepter de nouveaux éléments syntaxiques, qui seront ensuite transformés en C/C++ standard de la même manière que « C avec classes », ancêtre du C++, était d’abord transformé en C avant d’être compilé. Nous allons expliquer comment écrire une extension de la grammaire du C++ grâce au projet Transformers puis transformer le code étendu en code standard, en nous appuyant sur des exemples d’extensions déjà écrites (ContractC++, class-namespaces). Nous montrerons les avantages et inconvénients des technologies utilisées par Transformers comme les grammaires attribuées. COMPILATEUR TIGER * 16h45 : Intégration de techniques de parallélisation dans le compilateur Tiger –- Warren Seine Tiger est un langage utilisé à des fins pédagogiques dans l’étude des compilateurs. Écrite en C++, notre implémentation d’un compilateur Tiger profite de techniques éprouvées dans la transformation de programmes. L’ère du multi-coeur a rendu la parallélisation indispensable dans le cursus d’un étudiant en informatique. Utilisé comme support de cours, notre compilateur doit évoluer et tirer profit des nouvelles techniques de parallélisme. Ce rapport présente une solution pour distribuer le travail au sein d’un modèle de programmation concurrente par tâche. Nous utiliserons Intel Threading Building Blocks pour nous détacher des problématiques matérielles. -- Daniela Becker