Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les séminaires du LIFO

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 70 11
Fax: +33 (0)2 38 41 71 37



Les séminaires du LIFO


Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017

Sauf exception, les séminaires se déroulent le lundi de 14h à 15h, Salle de réunion 1, bâtiment IIIA (voir plan du campus).


09/12/2002 : Rule-based Constraint Propagation: Schedulers and Redundancy
Sebastian Brand (CWI Amsterdam) Résumé

02/12/2002 : Analyse de non-interférence pour processus mobiles par abstraction de sortes
Frédéric Prost (Équipe LEIBNIZ, IMAG, Grenoble) Résumé

18/11/2002 : Vérification formelle d'algorithmes parallèles sur réseaux d'interconnexion symétriques
Éric Gascard (LIFO, Orléans) Résumé

21/10/2002 : Requêtes sur objets répartis
Mourad Alia (France Télécom RD, Grenoble) Résumé

09/09/2002 : Sur le plongement et l'auto-complémentation cyclique des arbres
Pawel Wojda (LIFO et Université de Cracovie) Résumé

18/07/2002 : Soutenance de thèse : Construction de cartes pour l'exploration de corpus.
Isabelle Debourges (Lifo) Résumé
Attention : aura lieu à 15 heures, amphi H

02/07/2002 : Soutenance de thèse : Fouille de données par algorithmes génétiques
Agnès Braud (LIFO) Résumé
Attention : 15 heures, amphi H

03/06/2002 : Les systèmes embarqués : prise en compte des contraintes d'environnement dans les systèmes réactifs
Olivier Roux (IRCCyN, Ecole Centrale de Nantes) Résumé

13/05/2002 : Autour de la décomposition modulaire et des graphes bipartis
Jean-Marie Vanherpe (Université du Mans) Résumé

06/05/2002 : Apports de la Satisfaction de Contraintes à la Programmation Logique Inductive: un nouvel algorithme de théta-subsomption
Jérôme Maloberti (LRI - Université Paris 11) Résumé

09/04/2002 : Assuring Secrecy for Concurrent Declarative Programs
Rachid Echahed (CNRS - IMAG Grenoble) Résumé

18/03/2002 : Mémoire virtuellement partagée: des grappes vers la grille
Gabriel Antoniu (IRISA Rennes) Résumé

04/03/2002 : De nouveaux résultats sur l'analyse statique de programmes récursifs
Pierre Amiranoff et Albert Cohen (INRIA Rocquencourt) Résumé

28/01/2002 : Applications de la théorie des automates à divers problématiques du traitement informatique des langues
Denis Maurel (Université de Tours) Résumé


Résumés des séminaires


Rule-based Constraint Propagation: Schedulers and Redundancy Sebastian Brand, CWI Amsterdam

A constraint satisfaction problem (CSP) is a collection of relations, or constraints, on variables. A solution is a consistent assignment to the variables. The CSP concept is very general, and indeed the cost of solving CSPs can be exponential. One of the essential techniques for reducing the search space is constraint propagation. This can often be naturally formulated in a rule-based way. In this talk we first recall an abstract view of constraint propagation. We interpret it as fixpoint computation of monotonic and inflationary functions with a generic iteration algorithm. We then instantiate: our functions have the form of particular rules. The main part of the talk deals with a specialisation of the generic iteration algorithm for this class of rules. An implementation of the resulting rule scheduler performs well in experimental comparisons to CHR, the system of choice for rule-based constraint programming. Time permitting, we complement the above and discuss redundancy of rules. We propose a redundancy test, and demonstrate its usefulness in connection with automatic generation of constraint propagation rules.


Analyse de non-interférence pour processus mobiles par abstraction de sortes Frédéric Prost, Équipe LEIBNIZ, IMAG, Grenoble

Nous introduisons un nouveau calcul de processus mobiles inspire du calcul bleue de Boudol. Nous lui donnons un systeme de types dans la droite ligne des systemes "standard" des calculs fonctionnels, c'est a dire ou les types refletent la structure des termes. Nous montrons comment utiliser ce systeme de type pour obtenir une analyse statique polyvariante et donnons un resultat de non-interference qui peut etre utiliser dans de nombreuses applications (confidentialite, code mort, analyse des temps de liaison etc.).


Vérification formelle d'algorithmes parallèles sur réseaux d'interconnexion symétriques Éric Gascard, LIFO, Orléans

Je présenterais dans ce séminaire une partie des résultats de ma thèse, à savoir : une méthodologie de modélisation et de vérification d'algorithmes parallèles sur réseaux d'interconnexion symétriques. Nous utiliserons des techniques de preuve de théorèmes (theorem proving) et plus particulierement la preuve par induction. Les preuves seront paramétrés sur l'ordre du réseau (nombre de processeurs). L'exposé sera construit en quatre parties : 1) Modélisation formelle des réseaux symétriques dans un démonstrateur de théorèmes (Démonstrateur de Boyer&Moore utilisant une logique du 1er ordre + induction). Utilisation du formalisme des graphes de Cayley. 2) Modélisation et vérification fonctionnelle des primitives de communication collectives sur ces réseaux (broadcast, scatter, reduction, prefix-computation ....) 3) Modélisation et Vérification de programmes distribués 4) Exemples applicatifs sur l'hypercube : - Calcul parallèl du produit matrice-vecteur - Calcul parallèl du shape number d'une image Un des résultats principaux de ce travail est l'obtention automatique des invariants nécessaires aux preuves, ceci à partir de la notion de voisinage d'un processeur que nous avons formalisé.


Requêtes sur objets répartis Mourad Alia, France Télécom RD, Grenoble

Le sujet se situe dans le cadre de l'interrogation des sources de données hétérogènes (BD relationnelles, objet, annuaires, etc). La première partie de la présentation est un survol sur les travaux existants autours de ce thème. En deuxième partie, nous présentons un canevas (framework) de requêtes, Medor, que nous développons. L'approche suivie par Medor est celle d'un middleware adaptable et extensibles, permettant de manipuler des collections d'objets, et de traiter les références entre objets. Medor permet d'exprimer des requêtes et d'interroger plusieurs sources de données (hétérogènes). L'expression d'une requête se fait sous la forme d'un arbre, indépendamment d'un langage de requête en se basant sur une algèbre sur les objets. Cet arbre englobe à la fois l'expression de la requête et toutes les méta-données utiles pour l'optimisation et l'évaluation de cette requête. Nous distinguons les étapes classiques : réécriture, optimisation et évaluation. Nous terminons par des exemples d'intégration de Medor avec le service de persistance JORM pour une utilisation par JOnAS (serveur EJB d'ObjectWeb).


Sur le plongement et l'auto-complémentation cyclique des arbres Pawel Wojda, LIFO et Université de Cracovie

Tout a commencé en 1977-1978 quand plusieurs auteurs (Burns et Schuster, Bollobás et Eldridge, Ganter et Pelikan, Sauer et Spencer), ont indépendemment démontré le resultat suivant : THEOREME Soit G un graphe d'ordre n et taille n-2 (un (n,n-2)-graphe). Alors G est contenu dans son complément. Ce résultat est le meilleur possible puisque l'étoile K_{1,n-1} (donc un graphe d'ordre n et taille n-1) n'est pas contenu dans son complément. Je vais parler de résultats qui généralisent le théorème ci-dessus. S'il reste du temps, j'aimerais parler aussi d'autres résultats que j'ai obtenu (avec des co-auteurs) pendant mon séjour à Orléans qui s'achève...


Soutenance de thèse : Construction de cartes pour l'exploration de corpus. Isabelle Debourges, Lifo

Cette thèse s'inscrit dans une problématique qui intéresse principalement deux domaines de recherche en Informatique: il s'agit du Traitement Automatique des Langues d'une part et de l'Apprentissage Automatique d'autre part.


Soutenance de thèse : Fouille de données par algorithmes génétiques Agnès Braud, LIFO

La fouille de données est un processus visant à la découverte de connaissances potentiellement utiles, enfouies dans les bases de données. Parmi les problématiques de ce domaine, nous nous intéressons à l'apprentissage de concepts à partir d'exemples. Nous nous concentrons sur l'apprentissage de descriptions de concepts exprimées sous forme d'un ensemble de règles, et sur l'apport des algorithmes génétiques dans ce domaine. Ce travail se décompose en deux parties. Tout d'abord, nous proposons une approche génétique pour l'apprentissage de concepts dans un cadre relationnel. Cette approche repose sur un codage original des règles en logique du premier ordre. Une clause très générale est donnée comme schéma pour les règles à apprendre. L'apprentissage consiste alors à chercher des contraintes pertinentes sur les variables de ce schéma, et notamment des contraintes d'égalité. Dans notre approche, nous considérons la partition induite sur l'ensemble des variables. Un individu code une telle partition, les contraintes sur les valeurs des variables étant posées sur les classes d'équivalence. Des opérateurs génétiques inspirés des opérateurs ensemblistes sont définis pour faire évoluer une population de tels individus. Une étude de ces opérateurs montre que leur effet sur les individus auxquels ils s'appliquent se traduit au niveau des règles correspondantes par des transformations couramment utilisées en apprentissage. Le processus d'évolution permet d'ajuster la forme de la règle solution. Nous proposons un système, appelé GRIL, basé sur ces principes. Nous étudions ensuite le bénéfice de deux approches de parallélisation d'un algorithme génétique en termes d'accélération, en utilisant le modèle de programmation parallèle BSP. La première de ces approches consiste à répartir la population, la seconde à répartir la base de données. Les études théoriques permettent de prédire des accélérations significatives, résultats confirmés par les expérimentations. Mots-clés : apprentissage, algorithmes génétiques, fouille de données, classification, programmation logique inductive, propositionnalisation, parallélisme.


Les systèmes embarqués : prise en compte des contraintes d'environnement dans les systèmes réactifs Olivier Roux, IRCCyN, Ecole Centrale de Nantes

La programmation asynchrone des applications temps-réel nous a conduit à construire des modèles de comportements dans lesquels il est possible de prendre en compte des mémorisations (en nombre à priori illimité) d'événements (pour les cas où ceux-ci ne peuvent pas être pris en compte au moment de leur occurrence). C'est pourquoi nous avons conçu le modèle des automates à file réactifs (RFAs (Reactive FIFFO Automata)), qui sont dotés d'une structure de mémorisation sous la forme d'une file FIFFO (First In First Fireable Out). Ceci permet de traiter les événements enregistrés dés que possible et avec priorité au plus ancien (proche du FIFO classique). Nous présentons d'abord le modèle et nous montrons en quoi nous sommes préoccupés par la question de la non-bornitude de la file. Pour étudier complètement ce problème dans sa réalité, nous sommes amenés à prendre en compte les contraintes imposées par l'environnement sous la forme des rythmes d'occurrences des événements perçus.


Autour de la décomposition modulaire et des graphes bipartis Jean-Marie Vanherpe, Université du Mans

Se voulant résolument didactique l'exposé traitera en premier lieu d'une méthode de décomposition des graphes bien connue : la décomposition modulaire et présentera quelques classes de graphes où cette méthode montre son efficacité. L'examen d'analogies avec le cas des graphes bipartis conduira à présenter une méthode de décomposition spécifique à cette famille de graphes et à traiter de son application dans certaines sous-classes.


Apports de la Satisfaction de Contraintes à la Programmation Logique Inductive: un nouvel algorithme de théta-subsomption Jérôme Maloberti, LRI - Université Paris 11

La théta-subsomption est une restriction de la subsomption generalisée qui est décidable mais reste NP-difficile. La théta-subsomption est utilisée en PLI (Programmation Logique Inductive), elle est donc intensivement appelée au cours de l'apprentissage et une implantation efficace est nécessaire. Elle peut être reformulée comme un Problème de Satisfaction de Contraintes (PSC) très simplement et ainsi bénéficier des techniques de réduction et d'exploration developées dans ce domaine. Les PSCs conservent une complexité exponentielle dans les pires cas, mais la complexité effective n'atteint son maximum que dans une region étroite appelée la Transition de Phase (TP). Je vous présenterais un nouvel algorithme de théta-subsomption, appelé Django, utilisant des techniques issues des PSCs ainsi que des optimisations spécifiques. Django a été validé experimentalement sur des données se situant dans la TP afin d'observer ses performances dans les pires cas empiriques.


Assuring Secrecy for Concurrent Declarative Programs Rachid Echahed, CNRS - IMAG Grenoble

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels towards more sensitive ones. Our algorithm uses a terminating abstract operational semantics which reduces the problem of secrecy to constraint solving within finite lattices. It departs in that from the previous works essentially based on type systems. Furthermore, our proposal is general and tackles a very large class of programs which includes strictly those considered by Boudol and Castellani or Smith and Volpano.


Mémoire virtuellement partagée: des grappes vers la grille Gabriel Antoniu, IRISA Rennes

Dans leur présentation traditionnelle, les systèmes à mémoire distribuée virtuellement partagée (MVP, en anglais DSM) permettent à des processus de partager un espace d'adressage commun selon un modèle de cohérence fixé: cohérence séquentielle, relâchée, etc. Dans la plupart des travaux dans ce domaine, il est sous-entendu que la MVP et l'architecture sous-jacente sont données. Le programmeur doit alors adapter son application à ce cadre fixe, afin d'obtenir une exécution efficace. Dans une première partie de cet exposé, nous présenterons une plate-forme générique d'implémentation et d'expérimentation appelée DSM-PM2, qui permet de développer et d'optimiser à la fois les applications distribuées et le(s) protocole(s) de cohérence de la MVP sous-jacente. DSM-PM2 est une plate-forme logicielle, portable sur de nombreuses architectures de grappes hautes performances. Cette plate-forme fournit les briques de base nécessaires pour implémenter et évaluer une large classe de protocoles de cohérence multithreads dans un cadre unifié. Trois modèles de cohérence sont actuellement supportés: la cohérence séquentielle, la cohérence relâchée et la cohérence Java. La plate-forme a été validée par son utilisation en tant que cible d'un système de compilation Java pour des grappes de PC, appelé Hyperion. Des études comparatives de performance ont été effectuées sur 5 applications Java multithreads en utilisant diverses variantes du protocole de cohérence, sur plusieurs architectures différentes. Dans la deuxième partie de l'exposé, nous montrons pourquoi le passage à l'échelle des systèmes à mémoire virtuellement partagée, jusqu'ici conçus pour des grappes de petite taille, exige une remise en question des hypothèses traditionneles lorsqu'on se propose de prendre en compte des architectures à plusieurs milliers de noeuds répartis. Nous présentons une proposition d'architecture de service de partage de mémoire à grande échelle basée sur des techniques peer-to-peer. Pour plus d'informations: site DSM-PM2 ; page personnelle de Gabriel Antoniu


De nouveaux résultats sur l'analyse statique de programmes récursifs Pierre Amiranoff et Albert Cohen, INRIA Rocquencourt

Nous cherchons à améliorer la précision des analyses pour programmes récursifs. Cet exposé décrit plus particulièrement le calcul statique - lors de la compilation - des accès aux structures de données (arbres et tableaux). Nous introduisons le concept de variable d'induction généralisée, qui étend la notion classique attachée aux nids de boucles. Ce concept formalise le suivi des adresses au travers d'un balisage original de l'exécution. Dans le cas particulier de la parallélisation automatique, cette information est essentielle pour l'analyse de dépendances. Tout d'abord, nous dégageons la notion d'instance pour nommer avec exactitude une instruction au cours de l'exécution (nous définissons formellement ce concept). L'analyse par instances conjugue la finesse des traces d'exécution et la richesse d'expression du formalisme des langages réguliers. Le concept d'instance est ensuite appliqué à un modèle de programme qui permet le calcul exact des adresses accédées par chaque instance. Ce modèle présente une abstraction de l'adressage des structures de données à l'aide de monoïdes. Des algorithmes sont exposés, en étroite référence à la théorie des automates finis (transductions, matrices et équations récurrentes sur des semi-anneaux).


Applications de la théorie des automates à divers problématiques du traitement informatique des langues Denis Maurel, Université de Tours

L'analyse présyntaxique du langage naturel met en oeuvre la création et l'utilisation de lexiques, ainsi que le développement d'outils par l'intermédiaire de la théorie des automates à nombre fini d'états. La question centrale, dans cette approche du traitement du langage, est la suivante: que peut-on faire avant une analyse globale de la phrase? C'est dans ce sens qu'on peut définir la notion de préanalyse qui sous-tend l'ensemble de ce thème de recherche, comme tout ce qu'il est possible de faire au niveau local, avant d'aborder la complexité de la phrase elle-même. Les travaux réalisés dans ce sens au Laboratoire d'Informatique de Tours s'organisent autours de cinq directions de recherche : * Reconnaissance des adverbiaux de localisation * Traitement automatique des noms propres (Prolex) * Aide à la communication des personnes handicapées physiques (HandiAS) * Interrogation de bases de données en langue naturelle * Découverte de connaissances dans les textes