navigation

 


Résumés des démonstrations et posters

 

 


   Démo - Recherche adaptative et contraintes musicales
Auteur(s) :   Charlotte Truchet ( IRCAM)

Résumé : Nous présentons deux prototypes de solvers de contraintes dans OpenMusic. OpenMusic est un langage visuel pour la composition assistée par ordinateur basé sur Common Lisp/CLOS. Nous avons intégré à OpenMusic un solver par backtracking en Lisp, appelé Screamer (Screamer comporte aussi un solver par propagation qui sera ajouté ultérieurement). Parallèlement, nous présentons une implémentation d'un algorithme de recherche locale, appelé recherche adaptative, dans le domaine musical. La recherche adaptative reprend le principe de résolution par optimisation d'une fonction de coût, mais en affinant la notion de coût de manière à tenir compte du poids de chaque variable. Les deux solvers se complètent bien pour résoudre des problèmes musicaux.

Mots clés : programmation par contraintes, CSP, recherche locale, recherche adaptative, contraintes musicales, composition assistée par ordinateur, séries tous intervalles, Screamer


   Démo - Boosting et programmation logique inductive
Auteur(s) :   B. Gil   F. Noël   M. Sordi   N. Soules   S. Villefaunes ( IRIT - UMR CNRS 5505 - Université Paul Sabatier - Toulouse)

Résumé : La programmation logique inductive est un des multiples aspects de l'apprentissage. La méthode de boosting, initialement développée pour des classificateurs, consise à faire tourner en boucle une machine apprenante pour générer un nombre fini n d'hypothèses intermédiaires hi, i dans [1,n]. Entre chaque tour de boucle, les poids des exemples sont modifiés de manière ad-hoc. Le résultat final h est alors une combinaison linéaire des fonctions intermédiaires hi. On montre formellement que l'hypothèse finale h est plus performante que les hypothèses intermédiaires hi. D'où l'idée d'adapter la méthode à la programmation logique inductive et de valider le processus sur des bases de données de taille raisonnable. La démonstration que nous proposons consiste donc en l'exécution d'un prototype développé à l'IRIT Toulouse en 2 mois à partir d'un interprète Progol. Initialement développé à l'Université d'York, Progol est un des outils les plus répandus en apprentissage inductif. L'exécution en boucle de l'interprète, en faisant varier entre chaque boucle l'ensemble d'exemples, génère donc des hypothèses distinctes qui sont en fait des programmes logiques. A la fin de la procédure, un vote majoritaire est implanté pour choisir la réponse à une requête Q posée au système.

Mots clés : apprentissage, logique inductive, boosting


   Démo - Localisation des erreurs par slicing dans les programmes logiques avec contraintes
Auteur(s) :   Ulrich Neumerkel ( Université Technique de Vienne)

Résumé : Nous présentons des outils pour expliquer les phénomènes inattendus des programmes logiques avec contraintes (PLC). Lesdits outils s'appuient sur des lectures sélectives adaptées aux besoins éducatifs. Les techniques développées localisent des erreurs en déterminant un fragment exécutable du programme, appelé slice ou tranche. Afin d'enlever l'erreur dans le programme original, il est indispensable de modifier le fragment proposé par le système. Par contre, si on ne modifie que des parties hors du fragment, l'erreur persistera. Nos outils ont été intégrés dans un environnement de programmation spécialisé pour l'enseignement de la PLC, facilitant les lectures sélectives pour l'échec inattendu, les solutions inattendues et la non terminaison.


   Démo - TCLP: Programmes logiques avec contraintes typés
Auteur(s) :   Emmanuel Coquery ( INRIA Rocquencourt)

Résumé : TCLP est un programme de typage pour la programmation logique avec contraintes, utilisant le sous-typage et le polymorphisme paramétrique, basé sur la bibliothèque de sous-typage Wallace de F.Pottier. Son objectif est la détection statique d'erreurs de programmation. Il introduit une discipline de typage simple pour les programmes logiques avec contraintes qui autorise, via le sous-typage, les coercions usuelles entre les domaines de contraintes et le typage de la méta-programmation. TCLP lit des sources Prolog (ISO ou Sicstus), et effectue une vérification de types à l'aide de déclarations de types pouvant être incluses dans les sources à vérifier. Il est également possible d'inférer des types pour des prédicats non déclarés.

Mots clés : sous-typage, polymorphisme paramétrique, programmation logique, programmation par contraintes, vérification de types, inférence de types


   Démo - HyperPro - Un environnement intégré de documentation pour la PLC
Auteur(s) :   AbdelAli Ed-Dbali ( LIFO - Université d'Orléans)

Résumé : Le but de cette démonstration est de présenter certaines fonctionnalités du système HYPERPRO. HYPERPRO est un environnement de développement integré pour la PLC (programmation en logique et par contraintes) qui offre deux aspects du développement d'un programme : le codage en PLC et la documentation. Un document HYPERPRO est donc une combinaison de code et de sa documentation. La partie édition d'HYPERPRO est basé sur le système Thot. HYPERPRO est un éditeur WYSIWYG qui offre des facilités de navigation hypertexte, de manipulation de versions d'un même programme, d'extraction de vues projections selon des critères spécifiques. Il offre également l'exportation de document vers plusieurs formats courants (ps, html, latex, ...) ainsi que la gestion des indexes. HYPERPRO a été conçu pour la PLC mais il peut aussi bien être adapté à d'autres paradigmes de programmation.

Mots clés : PLC, programmation littéraire, gestion de versions, édition structurée, hypertexte, documentation, spécification


   Poster - GUPU - un environnement pour l'enseignement de Prolog et de la PLC
Auteur(s) :   Ulrich Neumerkel ( Université Technique de Vienne)

Résumé : GUPU est un environnement de programmation spécialisé pour l'enseignement de Prolog et de la programmation logique avec contraintes. Notre approche repose sur une technique de lecture sélective textuelle à plusieurs niveaux. Par rapport aux approche courantes, les aspects déclaratifs, comme également quelques propriétés opérationnelles essentielles - en particulier, la terminaison ainsi que la non terminaison - son expliqués tout en évitant les notions d'arbres de preuve et les traces. L'environnement GUPU a les caractéristiques suivantes:
- langage Prolog pur et extensions de la PLC, CLP(FD) de SICStus.
- intégration de toute activité de programmation dans une seule commande (sauvegarde, validation syntaxique, compilation, chargement, test d'assertions, pré-notation) permettant un retour immédiat par rapport à l'état du système.
- pratique d'écrire les test (assertions) puis coder - récement vulgarisée par le mouvement extreme programming - mettant l'accent sur la spécification du problème.
- pré-notation automatisée et instantanée.
- validation de la syntaxe (indentation, orthographe etc.) pour renforcer des standard de codage et remédier aux difficultés de la syntaxe édimbourgeoise fragile.
- inférence de condtions de terminaisons (cTI).
- vérification de la non-terminaison (NTI).
- explication des phénomènes inattendus pour supporter des lectures sélectives.
- affichage des graphismes sans effet de bords et animation du processus d'instantiation.
- messagerie intégrée dans le texte du programme.
- dialogues trilingues (allemand/français/anglais).




   Poster - Fractions : outils de vérification de propriétés par des techniques de
Auteur(s) :   Fabrice Parrennes ( Université Paris 6, LIP6 -- SURLOG S.A.)

Résumé : Ce poster présentera une technique de vérification de propriétés de programmes fondée sur la résolution de contraintes. Cette technique est utilisée pour des programmes réactifs de type contrôle commande. Ces programmes sont traduits auparavant, grâce à l'outil AGFLr (1), en une famille de programmes très simples, ne comportant que des affectations gardées. Cette classe de programmes peut être traduite vers un langage constitué d'un noyau impératif sans récursion. Les propriétés étudiées sont décrites dans le même langage et portent sur l'aspect fonctionnel/dysfonctionnel du programme étudié. L'outil Fraction implémente cette analyse. Il est basé sur une interprétation des propriétés d'un programme par des contraintes et une bibliothèque de simplification permet d'obtenir une forme normalisée des contraintes utilisées. On utilise alors des outils externes de vérification de contraintes pour valider plus finement les propriétés recherchées. L'utilisation de techniques liées aux contraintes pour la vérification des propriétés n'est pas véritablement nouvelle, que ce soit dans l'univers de la vérification de modèle ou dans des techniques de recherche de jeux de test logiciel. L'originalité de l'approche consiste à combiner une analyse statique de programme et une représentation sous forme de contraintes des propriétés. Les propriétés recherchées et les programmes analysés sont exprimés eux-mêmes dans un langage unique de contraintes. La validation de l'approche utilise des mécanismes semblables à ceux utilisés en interprétation abstraite, une correspondance entre contraintes et propriétés est établie et un algorithme de simplification (basée sur une sémantique à réduction des domaines) permet d'obtenir une forme normalisée où à chaque contrainte est associée un unique ensemble de valeurs. Dans ce cadre, la validation de l'abstraction d'une propriété se ramène alors à un problème de satisfaction de contraintes et les techniques habituelles d'interprétation abstraite permettent de conclure sur la validité de la propriété.
--
(1) AGFLr (Analyse par Graphe Fonctionnel du Logiciel) est un outil développé par SURLOG S.A.

Mots clés : vérification de propriétés, interprétation abstraite, résolution de



 

line
© INRIA (pour toute question ou suggestion sur le site écrire à A. ED-DBALI)

Informations pratiques (Hôtels, Restos, Transports, ...)Appel à démos et postersBulletin d'inscriptionNouveautés sur le siteAccueilWelcomeRésumés des communicationsConférenciers invitésInstructions aux auteursComité de programme et d'organisationProgramme scientifiqueAppel à communications Lieu de la conférence coordonnées