Bonjour,

nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE qui aura lieu le mercredi 13 mai 2009 à 14 heures en Amphi 2 au KB.

----------------------------------------------------------------------- Le programme :

*Vaucanson, Transformers et Spot*

http://publis.lrde.epita.fr/Seminar-2009-05-13

VAUCANSON

* 14h00 : Analyse de performances pour projets C++ -- Florent D'Halluin * 14h30 : Traitement curatif pour Vaucanson: un renforcement du concept d'automate -- Jérôme Galtier

TRANSFORMERS

* 15h15 : Ajout de la programmation par contrats au C++ avec Transformers -- Vincent Ordy * 15h45 : Une implémentation des conteneurs C++ avec SCOOL -- Warren Seine

SPOT

* 16h30 : Traduction d'une LTL étendue en TGBA dans Spot -- Damien Lefortier * 17h00 : La complémentation d'automates de Büchi -- Guillaume Sadegh

-----------------------------------------------------------------------

Les Résumés des exposés : **************************

VAUCANSON

14h00 : Analyse de performances pour projets C++ -- Florent D'Halluin

Vaucanson est une bibliothèque C++ de manipulation d'automates finis. Par rapport à son concurrent principal, OpenFST?, Vaucanson souffre d'importants problèmes de performances. Afin d'améliorer les performances de Vaucanson, il est nécessaire d'avoir des outils appropriés pour analyser le comportement de la bibliothèque en termes d'utilisation de temps CPU et de gestion de la mémoire. Jusqu'en Mars 2009, il n'existait pas d'outils de ce type pratiques à utiliser avec Vaucanson. CBS (C++ Benchmarking Suite) est une suite d'outils d'analyse de performances pour projets C++. Ces outils permettent de mesurer, d'afficher, et de comparer l'utilisation de ressources (temps, mémoire), dans un format accessible à l'utilisateur. Ils sont utilisés pour analyser Vaucanson afin de réécrire les algorithmes les moins efficaces.

14h30 : Traitement curatif pour Vaucanson: un renforcement du concept d'automate -- Jérôme Galtier

Vaucanson permet de manipuler des automates finis. La modélisation de ces objets occupe donc une place centrale dans 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. Nous exposerons ce qui peut être considéré comme un véritable nud gordien dans la modélisation actuelle: Vaucanson est par exemple incapable de choisir une implémentation pour un automate en fonction d'une de ses propriétés. La solution apportée restaure alors une modélisation saine et empêchera des erreurs de conceptions lors de la recherche de spécifications des algorithmes. Finalement, nous exposerons, entre autre, une série de spécialisations du concept d'automate, ainsi qu'un ensemble d'améliorations du modèle qui étaient autrefois trop couteuses à mettre en place.

TRANSFORMERS

15h15 : Ajout de la programmation par contrats au C++ avec Transformers -- Vincent Ordy

La programmation par contrats est un paradigme permettant de réduire le temps de débogage des programmes, en spécifiant des conditions qui doivent être vérifiées à l'entrée d'une fonction (préconditions) ou à sa sortie (postconditions). Dans les languages orientés objet, il est également possible de vérifier un ensemble de contraintes à chaque appel ou sortie d'une fonction membre (invariants de classe), et les conditions sont héritées à partir des classes parentes.

Le projet Transformers a pour but de faire de la transformation source à source sur des sources C et C++. Une extension pour introduire les contrats dans le C a déjà été écrite alors que l'analyse syntaxique du C++ n'était pas encore fonctionnelle.

Nous allons montrer comment écrire une extension de la grammaire du C++ dans le projet Transformers pour introduire le principe de contrat dans le C++, puis transformer le code étendu en C++ standard.

15h45 : Une implémentation des conteneurs C++ avec SCOOL -- Warren Seine

SCOOL est un langage dédié conçu pour faciliter le développement C++ de haut-niveau. Fondé sur le paradigme SCOOP mélangeant programmation générique et orientée-objet, il se démarque par une résolution statique des appels de fonctions membres et un système de concepts puissant.

Précédemment, une bibliothèque de conteneurs standards a été réalisée en C++ grâce à SCOOL. Cette implémentation demandait cependant une forte maitrise des méchanismes de SCOOP. Avec SCOOL, nous pouvons y arriver sans se préoccuper des détails, laissés au traducteur C++.

En se concentrant sur le développement de la bibliothèque en SCOOL et sur les changements nécessaires au langage et à son compilateur, nous comparerons les solutions originales et DSL et déterminerons si SCOOL est adapté au prototypage d'applications génériques.

SPOT

16h30 : Traduction d'une LTL étendue en TGBA dans Spot -- Damien Lefortier

Spot est une bibliothèque de model checking 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 deux algorithmes de traduction de LTL en TGBA, une des étapes principales de l'approche automate. Nous présentons une nouvelle traduction en TGBA d'une LTL étendue dont les opérateurs sont représentés par des automates finis, permettant ainsi à Spot de vérifier des propriétés qui n'étaient pas exprimables auparavant. Nous présenterons aussi de quelles façons nous pourrions intégrer certaines fonctionnalités de PSL (Property Specification Language) à notre extension.

17h00 : La complémentation d'automates de Büchi -- Guillaume Sadegh

Le model checking est un domaine de la vérification formelle, qui permet de vérifier le comportement d'un système à travers des formules logiques. 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. Pourtant, un algorithme est manquant : celui de la complémentation d'automates de Büchi (qui produit un automate reconnaissant la négation du langage initialement reconnu). Cet algorithme est peu utilisé dans la pratique à cause de sa forte complexité, mais il ne manque pas d'intérêt du point de vue théorique. Nous présenterons une implémentation d'un tel algorithme dans Spot.