• Summary
• LIFO Members (Directory)
• Research Teams
• CA
• GAMoC
• LMV
• Pamda
• SDS
• Research Actions
• Doctoral Research
• Seminars and Events
• Seminars (french)
• Events at LIFO
• Events out of LIFO
• Publications and Software
• Publications
• Doctoral and Habil. Theses
• Research Reports
• Software
• Technology transfer

• Contacts/Reaching LIFO
• Who's who at LIFO
• Coming to LIFO
• Teaching
• CS Department
• CS Technical Department
• INSA Centre-Val de Loire

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 99 29
Fax: +33 (0)2 38 41 71 37

LIFO seminars (french)

15/12/2004 : Higher-Order Program Transformation based on Rewriting Induction
Yoshihito Toyama (Tohoku Unverity, Japan) Résumé
Attention : 14h salle de Réunion 1

08/12/2004 : Une méthode de classification non-supervisée pour l'apprentissage de règles et la recherche d'information
Guillaume Cleuziou (LIFO) Résumé
Attention : Soutenance de thèse à 14h Amphi Herbrand

07/12/2004 : Modèles opérationnels communicants, performances et algèbres de chemins
Armelle Merlin (LIFO) Résumé
Attention : Soutenance de thèse à 14h Amphi Herbrand

06/12/2004 : Langages d'arbres réguliers et algébriques pour la réécriture et la vérification.
Julie Vuotto (LIFO) Résumé
Attention : Soutenance de thèse à 14h Amphi 4

06/12/2004 : Learning in AL-log: Theory, Implementation, and Applications
Francesca Lisi (Université de Bari) Résumé
Attention : A 11h salle Réunion 1

29/11/2004 : A gentle Introduction into the Calendar and Time Type System CaTTS.
Stephanie Spranger (Munich) Résumé

08/11/2004 : Coupling et auto-stabilisation.
Stéphane Messika (LSV - ENS Cachan) Résumé

11/10/2004 : An on-line incremental approach for dynamically maintaining chordal graphs.
Yngve Villanger (Bergen, Norvège) Résumé

17/09/2004 : Soutenance de thèse.
Julien Arsouze (LIFO) Résumé
Attention : Soutenance de thèse, 14h30, amphi S

07/05/2004 : Branchwidth des graphes d'intervalles circulaires.
Frédéric Mazoit (LIP - ENS Lyon) Résumé

23/04/2004 : Contraintes et fouille de données.
Teddy Turmeaux (LIFO) Résumé
Attention : Soutenance de thèse. Commencera à 14h30, amphi S.

19/04/2004 : Calculer géométriquement sur le plan : machines à signaux.
Jérôme Durand-Lose (LIP - ENS Lyon et I3S - Université de Nice - Sophia Antipolis) Résumé

19/04/2004 : Algorithmes de tris paralleles pour clusters / developpement d'un gestionnaire SQL.
Christophe Cérin (Université de Picardie) Résumé

05/04/2004 : Extraction d'informations à partir de données à l'aide de modèles probabilistes et de noyaux.
Florence d'Alché-Buc (Université Pierre et Marie Curie, Paris & Genopole, Evry) Résumé

05/04/2004 : Algorithmes sélectifs de recherche.
Tizian Cazenave (Université Paris 8) Résumé

29/03/2004 : Construction de programmes parallèles par des techniques de transformations.
Eric Violard (LSIIT-ICPS, ULP Strasbourg) Résumé

22/03/2004 : Un système de types dépendants pour le calcul des Ambiants.
Cedric Lhoussaine (University of Sussex) Résumé

15/03/2004 : Outils de Visualisation et d'Immersion en Réalité Virtuelle pour la Télé-Micromanipulation en Temps-Réel.
Antoine Ferreira (LVR, ENSI Bourges) Résumé

23/02/2004 : Ordres cycliques pour digraphes fortement connexes, preuve d'une conjecture de Gallai.
Stéphane Bessy (LaPCS, Université Lyon 1) Résumé

16/02/2004 : Le rôle des contraintes dans les théories linguistique.
Philippe Blache (Laboratoire Parole et Langage, Aix-en-Provence) Résumé

02/02/2004 : Preuves d'équivalence de programmes logiques.
Sorin Craciunescu (INRIA Rocquencourt) Résumé

26/01/2004 : Bornes polynômiales pour la largeur arborescente.
Etienne Birmelé (LAPCS, Université Lyon 1) Résumé

12/01/2004 : Certification de vérificateur de bytecode.
Pierre Courtieu (LIFO - Bourges) Résumé

Résumés des séminaires

Higher-Order Program Transformation based on Rewriting Induction Yoshihito Toyama, Tohoku Unverity, Japan
A rewriting induction approach to the fusion transformation of functional program is introduced. From a given program the fusion transformation involves finding equations as inductive theorems which make a new efficient program. We give a procedure for the fusion transformation based on rewriting induction by Reddy (1990). Using the framework of S-expression rewriting system (SRS), fusion transformations of higher-order rewriting systems is easily realized through rewriting induction which is improved for this purpose. We also discuss the correctness of the procedure.

Une méthode de classification non-supervisée pour l'apprentissage de règles et la recherche d'information Guillaume Cleuziou, LIFO
Le regroupement d'objets, dans un cadre non-supervisé, est une tâche importante et difficile en apprentissage. Ce processus intervient dans des contextes variés tels que la découverte de connaissances, la simplification dans le représentation ou la description d'un ensemble de données. Nous proposons, dans cette étude, l'algorithme de clustering PoBOC permettant de structurer un ensemble d'objets en classes non-disjointes. Nous utilisons cette méthode de clustering comme outil de traitement dans deux applications très différentes. - En apprentissage supervisé, l'organisation préalable des instances apporte une connaissance utile pour la tâche d'induction de règles propositionnelles et logiques. - En Recherche d'Information, les ambiguïtés et subtilités de la langue naturelle induisent naturellement des recouvrements entre thématiques. Dans ces deux domaines de recherche, l'intérêt d'organiser les objets en classes non-disjointes est confirmé par les études expérimentales adaptées.

Modèles opérationnels communicants, performances et algèbres de chemins Armelle Merlin, LIFO
Nous développons et étendons le modèle BSP (Bulk Synchronous Parallelism) qui permet une programmation data-parallèle explicite et un calcul de coût simple. Nous exposons d'abord des machines virtuelles pour le langage BSML associant BSP, programmation fonctionnelle et estimation des performances. Nous proposons ensuite d'associer concurrence et parallélisme. Ceci à l'aide d'une extension de l'algèbre de processus CCS, nommée BSPA, qui préserve les caractéristiques de BSP. Nous associons à BSPA un modèle de coût basé sur les algèbres de chemins et fidèle au modèle de performance BSP. Nous montrons comment appliquer ce modèle aux problèmes d'ordonnancement posés par l'informatique globalisée ou meta-computing. Cette méthode de calcul de coût est générale et peut s'appliquer à d'autres algèbres de processus. Ainsi nous proposons un modèle de dépense de ressources mémoire pour l'algèbre de processus SPPA dédiée aux protocoles cryptographiques et en particulier au protocole TCP.

Langages d'arbres réguliers et algébriques pour la réécriture et la vérification. Julie Vuotto, LIFO
Partant d'un système de réécriture R basé sur les constructeurs et d'un langage initial E, il est alors possible de calculer l'ensemble des descendants, c-à-d des termes atteignables à partir de E en appliquant récursivement les règles de R. Calculer l'ensemble des descendants peut être utilisé aussi bien en réécriture (notamment pour vérifier certaines propriétés comme l'accessibilité et la joignabilité) qu'en vérification de protocoles cryptographiques. Les travaux de P. Réty portent sur un calcul d'un ensemble exact de descendants réguliers. Nous les avons étendus en prenant en compte des stratégies de réécriture (innermost, outermost, leftmost et leftmost-innermost). Procéder à un calcul exact nécessitant des restrictions sur R et sur E, nous avons étudié les descendants à travers un langage plus expressif : les langages algébriques d'arbres.

Learning in AL-log: Theory, Implementation, and Applications Francesca Lisi, Université de Bari
Many real-world applications require nowadays a unified approach to both relational and structural data. Hybrid systems for knowledge representation and reasoning that combine (fragments of) Horn clausal logic and Description Logics, notably CARIN and AL-log, have been invented to satisfy this requirement. Yet they are poorly investigated in research areas like machine learning (in particular, ILP) that could benefit from their augmented expressive and deductive power to face new challenging applications. In this seminar I shall present a framework for learning in AL-log, its implementation in the system AL-QuIn for frequent pattern discovery at multiple levels of description granularity, and the applications of AL-QuIn in Spatial Data Mining and Semantic Web Mining.

A gentle Introduction into the Calendar and Time Type System CaTTS. Stephanie Spranger, Munich
This talk introduces into the Calendar and Time Type System CaTTS. CaTTS goes far beyond predefined date and time types after the Gregorian calendar. CaTTS gives rise to declaratively specify cultural or professional calendars including specificities such as leap seconds, leap years, and time zones. CaTTS offers a tool for static type checking of data typed after calendar(s) defined in CaTTS and a language and solver for declaratively expressing and efficiently solving temporal constraints referring to calendar(s) expressed in CaTTS. CaTTS complements data modeling and reasoning methods designed for generic Semantic Web applications such as RDF or OWL with methods specific to the particular application domain of calendars and time.

Coupling et auto-stabilisation. Stéphane Messika, LSV - ENS Cachan
A randomized self-stabilizing algorithm A is an algorithm that, whatever the initial configuration is, reaches a set L of legal configurations in finite time with probability 1. The proof of convergence towards L is generally done by exhibiting a potential function f, which measures the ``vertical'' distance of any configuration to L, such that f decreases with non-null probability at each step of A. We propose here a method, based on the notion of coupling, which makes use of a ``horizontal'' distance d between any pair of configurations, such that d decreases in expectation at each step of A. In contrast with classical methods, our coupling method does not require the knowledge of L. In addition to the proof of convergence, the method allows us to assess the convergence rate according to two different measures. Proofs produced by the method are often simpler or give better upper bounds than their classical counterparts, as examplified here on Herman's mutual exclusion and Iterated Prisoner's Dilemma algorithms in the case of cyclic graphs. Voir aussi : http://www.lsv.ens-cachan.fr/~messika/perso.php

An on-line incremental approach for dynamically maintaining chordal graphs. Yngve Villanger, Bergen, Norvège
A graph G is chordal (or triangulated) if every cycle of length at least four contains an edge between two non-consecitive vertices of the cycle. For a chordal graph G, we study the problem of whether a new vertex u and a given set of edges between u and vertices of G can be added to G so that the resulting graph remains chordal. We show how to resolve this efficiently, and at the same time, if the answer is no, define a maximal subset of the proposed edges that can be added, or conversely a minimal set of extra edges that should be added in addition to the given set. In order to do this, we give a new characterization of chordal graphs and, for each potential new edge (u,v), a characterization of the set of edges incident to u that also must be added to G along with (u,v). We propose a data structure which can compute and add each such set in O(n) time. Based on these results, we present a new algorithm which computes both a minimal triangulation and a maximal chordal subgraph of an arbitrary input graph in O(nm) time. This time complexity matches the best known time bound for minimal triangulation, using a totally new vertex incremental approach. In opposition to previous algorithms, our process adds each new vertex without reconsidering any choice made at previous steps, and without requiring any knowledge of the vertices that might be added at further steps, which makes it the first fully on-line algorithm for these problems.

Soutenance de thèse. Julien Arsouze, LIFO

Branchwidth des graphes d'intervalles circulaires. Frédéric Mazoit, LIP - ENS Lyon
La notion de branchwidth a été introduite au début des année 90 par Robertson et Seymour comme obstruction à la treewidth (largeur arborescente). On peut montrer que bw(G)<=tw(G)+1<=3/2br(G). Seymour et Thomas ont montré que le branchwidth des graphes planaires est calculable en temps polynomial fournissant ainsi la meilleure approximation de la treewidth des graphes planaires. Depuis, relativement peu de personne se sont intéressés à cette forme de décomposition. Après avoir introduit les décompositions en branches et la branchwidth, je présenterai un théorème de calcul général du branchwidth puis son application aux graphes d'intervalles circulaires.

Contraintes et fouille de données. Teddy Turmeaux, LIFO
La fouille de données est un domaine de recherche actif, visant à découvrir des connaissances implicites dans des bases de données. Nous étudions l'intérêt de différents formalismes pour les connaissances et les données. En particulier, nous examinons l'intérêt des contraintes, formules du premier ordre interprétées sur un domaine particulier. Nous nous intéressons à la fouille de données dans les BD contraintes, BD qui étendent les BD relationnelles, déductives et spatiales en permettant la définition d'ensembles infinis. Nous étudions ensuite le bénéfice des clauses contraintes. Nous reprenons la définition classique de généralité entre ces clauses et nous déterminons dans ce cadre le moindre généralisé, le moindre spécialisé et d?autres opérateurs de raffinement utiles en fouille de données. Enfin nous introduisons un nouveau motif: les règles caractéristiques. Nous montrons leur intérêt dans le cadre de BD géographiques, notamment sur des données géologiques fournies par le BRGM.

Calculer géométriquement sur le plan : machines à signaux. Jérôme Durand-Lose, LIP - ENS Lyon et I3S - Université de Nice - Sophia Antipolis
Cet exposé se place dans l'étude des modèles du calcul continus. Nous y montrons que la géométrie plane permet de calculer. Nous définissons un calcul géométrique et utilisons la continuité de l'espace et du temps pour stocker de l'information au point de provoquer des accumulations. Dans le monde des automates cellulaires, on parle souvent de particules ou de signaux (qui forment des lignes discrètes sur les diagrammes espace-temps) tant, pour analyser une dynamique que, pour concevoir des automates cellulaires particuliers. Le point de départ de nos travaux est d'envisager des versions continues de ces signaux. Nous définissons un modèle de calcul continu, les machines à signaux, qui engendre des figures géométriques suivant des règles strictes. Ce modèle peut se comprendre comme une extension continue des automates cellulaires. L'exposé commence par une présentation des automates cellulaires et la mise en avant d'exemples de particules/signaux tirés de la littérature. De là, nous abstrayons le modèle, les machines à signaux. Dans un premier temps, nous montrons comment tout calcul au sens de Turing (par la simulation de tout automate à deux compteurs) peut y être mené. Nous montrons également comment modifier une machine de manière à réaliser des transformations géométriques (translations, homothéties) sur les diagrammes engendrés. Nous construisons également les itérations automatiques de ces constructions de manière à contracter le calcul à une bande (espace borné) puis, à un triangle (temps également borné). Dans un second temps, nous nous intéressons aux points d'accumulation. Nous montrons que la prévision de l'apparition d'une accumulation est indécidable. Ce problème est même $\Sigma_20$-complet (hiérarchie arithmétique), en construisant pour tout automate à deux compteurs une machine à signaux et une configuration initiale simulant l'automate pour toutes les valeurs possibles. Nous prenons ensuite un point de vue statique, et non plus dynamique, sur les diagrammes espace-temps engendrés (de même qu'entre automates cellulaires et pavages). Pour chaque position, la valeur doit correspondre au voisinage sur un ouvert suffisamment petit. Muni de cet outil, nous regardons les plus simples accumulations possibles (les singularités isolées) et proposons un critère pour y « prolonger » le calcul. L'exposé se conclut par la présentation de perspectives de recherches. Le mémoire de l'HDR est accessible par : http://perso.ens-lyon.fr/jerome.durand-lose/Hdr/

Algorithmes de tris paralleles pour clusters / developpement d'un gestionnaire SQL. Christophe Cérin, Université de Picardie
Cet expose, composé de deux parties, abordera la problematique du tri parallele sur clusters afin de garantir des proprietes d'equilibrage des charges et des garanties sur les temps d'execution. Nous commencons par une discussion sur une famille d'algorithmes concus pour le cas homogene puis nous interessons au cas ou les processeurs ont des vitesses differentes. Apres une discussion sur l'equilibrage des donnees sur chacun des processeurs, nous examinerons une techniaue de distribution des donnees pour que les processeurs terminent en meme temps. La deuxieme partie sera consacree au developpement d'un gestionnaire SQL qui utilise des arbres de radicaux comme structure de base (et pas des B-arbres). Cette deuxieme partie fait reference a notre travail dans le cadre du projet Grid-Explorer dans lequel nous avons propose de deployer un service SQL sur la grille. Notre travail est pour l'instant situe tres en amont d'une integration des gestionnaires habituels (Oracle, MySql etc) dans la grille. Nous developpons une version multithreadee des operations de base de gestion des arbres de radicau (union, intersection, multiplication par une constante...). De nombreuses sources de parallelisme seront montres ainsi que les applications potentielles de ce gestionnaire en Data mining, notamment pour la decouverte de regles d'association. Enfin, les deux parties seront re-connectees en remarquant par exemple que l'operation de jointure des bases de donnees peut s'implementer par un tri.

Extraction d'informations à partir de données à l'aide de modèles probabilistes et de noyaux. Florence d'Alché-Buc, Université Pierre et Marie Curie, Paris & Genopole, Evry
L'apprentissage automatique s'avère particulièrement intéressant lorsqu'il fournit à l'utilisateur des informations lisibles et facilement interprétables. Longtemps l'apprentissage numérique s'est concentré sur des modèles mathématiques de type "boîtes noires" dont l'interprétation était difficile.Nous nous intéressons dans cet exposé à deux familles d'outils qui permettent l'extraction ou l'insertion d'informations dans un cadre numérique. Les modèles graphiques (probabilistes) forment la première famille d'outils qui s'appliquent dès que l'on souhaite modéliser la distribution de variables liées par des relations de dépendance conditionnelles. Des réseaux bayésiens aux modèles de mélange, ils offrent un cadre formel riche pour la modélisation. Les méthodes à noyaux constituent la seconde famille d'outils. Elles s'appuient sur la définition d'une fonction de similarité particulière, appelée noyau, qui correpond au calcul d'un produit scalaire dans un espace de Hilbert. Le principe est donc le suivant: on change d'espace de représentation en choisissant un noyau tel que dans le nouvel espace, le problème à résoudre sera plus facile. Cette astuce est principalement utilisée pour linéariser des problèmes non linéaires; elle peut aussi être employée pour traiter numériquement des données structurées en définissant un noyau basé sur une comparaison structurelle. Après avoir proposé un cadre méthodologique pour l'apprentissage, nous montrons comment utilsier ces deux familles d'outils pour deux types de modélisation: la modélisaiton de mots et de documents. Par souci de clarté, nous développerons essentiellement deuxième question qui concerne nos travaux les plus récents. En conclusion, nous proposerons des voies de recherches à l'intersection de l'apprentissage symbolique et de l'apprentissage numérique.

Algorithmes sélectifs de recherche. Tizian Cazenave, Université Paris 8
Je montre comment je suis parti d'une approche de l'amélioration de la résolution de problème basée sur l'apprentissage par auto-observation pour évoluer vers la génération automatique de programmes en utilisant la métaprogrammation logique, et ensuite vers des algorithmes de recherche sélectifs. La comparaison des différents choix possibles de représentation des métaprogrammes m'ont amené à trouver une équivalence entre les programmes de recherche engendrés automatiquement et un algorithme de recherche original, basé sur des connaissances abstraites, et plus efficace que les algorithmes existant jusqu'alors pour de nombreux jeux. Cet algorithme et ses améliorations ont permis de résoudre des jeux comme le Phutball 11x11 et l'Atari-Go 6x6, et sont très utiles pour les sous jeux du jeu de Go. Afin de l'appliquer à de nombreux problèmes et de comparer les algorithmes entre eux je développe une librairie d'algorithmes génériques pour l'Intelligence Artificielle.

Construction de programmes parallèles par des techniques de transformations. Eric Violard, LSIIT-ICPS, ULP Strasbourg
Beaucoup d'applications nécessitent des niveaux de performance que seules les architectures parallèles permettent d'atteindre. Cependant, programmer ces applications en visant ces architectures et de façon à exploiter efficacement leur puissance de calcul demeure un problème difficile. Il est indispensable de disposer d'outils formels basés sur certaines notions mathématiques pour aider le programmeur ou le compilateur à "raisonner" afin d'élaborer des programmes parallèles de qualité. Un tel raisonnement repose sur des transformations formelles d'"énoncés". Mes recherches concernent la définition de telles transformations et portent sur ces questions de raisonnement et méthodologie pour construire les programmes parallèles. Nous avons développé le cadre formel PEI, originairement conçu pour unifier deux approches classiques : le raffinement de programmes et la synthèse de programmes à partir de systèmes d'équations récurrentes et nous avons montré qu'il constitue un bon cadre pour la conception de programmes parallèles. Notamment, les objets PEI intègrent une notion abstraite de géométrie qui permet de relier le problème à l'architecture. Parmi les différents modèles de programmation qui ont été proposés par ailleurs, le data-parallélisme possède d'indéniables qualités en terme d'indépendance vis-à-vis de l'architecture, de clarté et de facilité d'écriture des programmes : un programme data-parallèle est principalement un programme séquentiel avec des expressions spécifiques pour décrire la localité des données. Cependant il semble assez difficile de conduire un raisonnement menant à une implantation efficace avec les langages data-parallèles standards HPF et C*. De plus, ces langages utilisent des sémantiques intuitives différentes pour les expressions de la localité des données. Ces différences justifient l'introduction d'un domaine sémantique pour les langages data-parallèles. Nous avons défini un tel domaine sémantique à partir de PEI et nous avons montré que ce domaine sémantique est bien adapté pour conduire le raisonnement menant à une implantation efficace sur une architecture cible. Mes travaux les plus actuels s'inscrivent dans le cadre du projet TAG de l'ACI GRID et le projet INRIA CALVI. Ils concernent respectivement la programmation des grilles de calcul et la simulation numérique de problèmes physiques modélisés par des équations aux dérivées partielles. Nous développons des transformations de code afin de circonscrire les nouveaux problèmes sous-jacents : hétérogénéité des ressources de calcul, conception des structures de données à utiliser, etc. Mes résultats sont obtenus sur la base de mes précédents travaux théoriques. Mots-clefs : algorithmique parallèle, modèle de programmation parallèle, data-parallélisme, grille de calcul.

Un système de types dépendants pour le calcul des Ambiants. Cedric Lhoussaine, University of Sussex
Le calcul des Ambiants est aujourd'hui une référence en matière de modélisation des systèmes distribués et mobiles, et a été la source de nouvelles idées pour le contrôle de l'accès aux ressources. Dans ce calcul, un ambiant représente une unité d'exécution nommée pouvant contenir elle-même d'autres ambiants et/ou être contenue dans un autre ambiant. Les processus de cette unité peuvent la faire migrer d'un ambiant englobant à un autre. Dans ce cadre, des systèmes de types ont été développés pour assurer des polices de sécurité élémentaires (e.g. interdiction pour tel ambiant d'accéder à tel autre ambiant). Ces dernières sont exprimées par les types et indirectement via une classification des ambiants dans des "groupes". Dans cet exposé nous présenterons une théorie alternative de "types dépendants" pour le calcul des Ambiants qui permet une plus grande flexibilité dans l'expression des polices de sécurité vis-à-vis des systèmes utilisant la notion de groupes. Cette théorie a également l'avantage de simplifier la spécification des polices de sécurité (ce qui ainsi facilite la vie du programmeur) et relègue la complexité inhérente à la vérification dans les règles de typage.

Outils de Visualisation et d'Immersion en Réalité Virtuelle pour la Télé-Micromanipulation en Temps-Réel. Antoine Ferreira, LVR, ENSI Bourges
L'objectif des recherches en Microrobotique au Laboratoire Vision et Robotique (LVR) de Bourges est centré sur l'élaboration d'interfaces multi-modales homme/machine permettant d'améliorer le triptyque « Perception - Communication - Interaction » entre l'opérateur et le micro/nano monde en incluant de nouveaux moyens d'interaction (voix, son, vision, haptique). Ces nouvelles interfaces homme/machine (IHM) ont pour rôle d'assister l'opérateur dans ses tâches de manipulation en lui fournissant une aide contextuelle et parfaitement bien adaptée aux contraintes du micromonde (effets d'échelle liées aux microforces, environnement contraint, tâches semi-automatisées...). Différents travaux dans ce domaine ont déjà montré que les techniques de réalité virtuelle (RV) combinées avec des méthodes d'asservissement visuelles permettent d'augmenter considérablement les interactions homme/machine dans divers domaines : assemblage de pièces micromécaniques, micromanipulation de cellules biologiques et bio-nanotechnologies. Les interfaces présentées dans cet exposé reposent sur des techniques de virtualisation du micromonde réel. Ces méthodes sont encore à l'heure actuelle peu utilisées compte tenu du niveau de modélisation relativement élevé. La reconstruction 3D de la scène constitue la première étape pour cette virtualisation du micromonde. Dans ce but, nous avons développé des algorithmes de traitement d'image, quasi temps-réel, capable de reconnaître les différents constituants de la scène et de les ré-actualiser. Une fois la scène reconstruite, nous proposons plusieurs méthodes de navigation tridimensionnelles avec différents niveaux d'immersion (2D et 3D). L'opérateur peut alors explorer intuitivement la scène, améliorer sa compréhension des phénomènes physiques à l'échelle micrométrique et contrôler la bonne exécution des opérations. Ce dernier est assisté dans ces tâches par une aide visuelle en ligne lui permettant d'augmenter sa perception du micromonde à travers du texte, du son ou des images. Après une phase de reconstruction 3D, un module de planification de trajectoires, optimisé vis à vis des contraintes de la scène (micro-objets, obstacles, lumière) est proposé. Une fois la trajectoire choisie, le geste de l'opérateur est alors guidé par des champs de potentiels virtuels symbolisant les différentes interactions avec les micro-objets. Le niveau ultime d'immersion sensorielle de l'opérateur, autrement dit lorsqu'il est « Télé-Présent » dans le micromonde, fait actuellement face à des contraintes technologiques liées essentiellement à la communication temps-réel au niveau de la reconstruction 3D des modèles physiques, de la parallèlisation des communications, des interactions homme/machine, et de la virtualisation 3D du monde réel. Cet exposé vise à présenter l'activité de recherche dans ce domaine au niveau international ainsi qu'au sein du LVR avec un aperçu des différentes problématiques de recherche rencontrées pour aborder la « Perception - Communication - Interaction » dans le nanomonde.

Ordres cycliques pour digraphes fortement connexes, preuve d'une conjecture de Gallai. Stéphane Bessy, LaPCS, Université Lyon 1
Une énumération d'un digraphe D fortement connexe à n sommets est une bijection entre les sommets de D et les sommets de G_n, un n-gone du plan. Un ordre cyclique est alors une classe de représentations cycliques stable par deux opérations: rotation des sommets de D sur G_n et échange de deux sommets de D consécutifs sur G_n et non reliés dans D. Ces opérations sont définies de façon à laisser invariant l'indice d'un circuit de D dans une énumération, c'est-à-dire le nombre de tours du circuit dans G_n, comptés dans le sens direct. La définition d'équivalents cycliques pour la stabilité, le 'feedback arc set' et le nombre chromatique permet l'énoncé de trois théorèmes min-max. Le premier de ces théorèmes implique que tout digraphe fortement connexe D est couvrable par \alpha(D) circuits, où \alpha(D) est la stabilité de D. Ceci répond à une conjecture de T. Gallai, posée en 1963. Le dernier des théorèmes est une généralisation d'un résultat de J.A. Bondy de 1976: tout digraphe D fortement connexe a un circuit de longueur au moins \chi(D), où \chi(D) est le nombre chromatique de D.

Le rôle des contraintes dans les théories linguistique. Philippe Blache, Laboratoire Parole et Langage, Aix-en-Provence
Les contraintes sont désormais au coeur de la représentation de l'information linguistique : toutes les théories modernes, quel que soit le domaine abordé (phonologie, syntaxe, sémantique, etc.), y font référence. Quelques unes en font un usage intensif. Je dresserai dans cet exposé un panorama des contraintes à travers quelques théories linguistiques en soulignant leur rôle dans l'analyse, allant du filtrage à la satisfaisabilité. Je montrerai ensuite comment l'utilisation des contraintes permettent de dépasser les limites des théories génératives et peuvent constituer une véritable alternative aux stratégies d'analyse classiques. En particulier, elles permettent de déplacer la question de la grammaticalité, en ouvrant ainsi la possibilité de rendre compte de tout énoncé, quelle que soit sa forme. Je terminerai en montrant comment cette approche permet d'expliquer des phénomènes linguistiques complexes comme la variabilité.

Preuves d'équivalence de programmes logiques. Sorin Craciunescu, INRIA Rocquencourt
Le but de ce travail est de proposer un système formel pour prouver que l'ensemble des succès d'un programme logique est inclus dans l'ensemble correspondant d'un autre programme. Cela permet de prouver que deux programmes logiques, un qui représente la spécification et un représentant l'implantation sont équivalents. Le langage logique considéré est CLP\forall qui est le langage de programmation logique avec contraines (CLP) auquel est ajouté le quantificateur universel. Nous présentons les sémantiques des succès finis et infinis et montrons qu'elles sont données par le plus petit et le plus grand point fixe du même opérateur. Un système de preuve pour l'inclusion des succès finis est présenté. Le système utilise pour les opérateurs et les quantificateurs logiques les mêmes règles que la logique du premier ordre. Pour raisonner sur les prédicats récursifs le système contient une règle d'induction. Nous prouvons la correction du système sous certaines conditions. Un système analogue pour l'inclusion des succès infinis est présenté. La règle d'induction est remplacée par une règle de coinduction. La correction est démontrée sous conditions analogues. Le deux systèmes sont équivalents sous certains conditions. Une implantation a été réalisée sous la forme d'assistant de preuve écrit en Prolog. Le programme a environ 4000 lignes et contient des procédures simples mais efficaces de recherche de preuves. Nous présentons des exemples de preuves réalises avec ce programme parmi lesquels la preuve de correction de quicksort.

Bornes polynômiales pour la largeur arborescente. Etienne Birmelé, LAPCS, Université Lyon 1
Robertson et Seymour ont introduit les décompositions arborescentes qui constituent un outil puissant pour l'étude de graphes, tant d'un point de vue théorique qu'algorithmique. En effet, de nombreux problèmes NP-complets deviennent polynômiaux quand on se restreint aux classes de graphes admettant une décomposition de largeur bornée. Cependant, si Robertson et Seymour ont montré que de telles classes se caractérisent par des mineurs planaires interdits, leurs bornes sont doublement exponentielles en la taille de ces mineurs, ce qui contribue à rendre les algorithmes inutilisables. En considérant trois manières différentes d'appréhender les décompositions arborescentes, nous donnerons des bornes polynômiales pour la largeur arborescente des graphes sans longs circuits ou sans prismes.

Certification de vérificateur de bytecode. Pierre Courtieu, LIFO - Bourges
Les cartes à puces de nouvelle génération intègrent des fonctionnalités complexes, notamment la possibilité de contenir plusieurs applets qui peuvent être téléchargées sur la carte après sa mise en vente. Ces nouvelles fonctionnalités amènent de nouveaux problèmes de sécurité, en particulier concernant la détection d'applets frauduleuses, la confidentialité des données entre applets etc. La plate-forme Javacard est l'architecture la plus utilisée pour ces cartes à puces. Son système de sécurité est basé sur l'utilisation d'un vérificateur de bytecode (BCV). Le BCV est un programme (en principe embarqué sur la carte) qui effectue des vérifications sur l'applet téléchargée avant d'autoriser son installation. Les vérifications effectuées concernent le typage correct des opérations, le confinement des données entre applets, l'initialisation des objets avant leur utilisation etc. La certification rigoureuse du BCV est évidemment un prérequis indispensable à la diffusion des nouvelle cartes à puce. Je présenterai la méthodologie et l'outil (appelé Jakarta), que nous avons conçus à l'INRIA Sophia Antipolis, qui permet d'effectuer cette certification en utilisant un assistant de preuve pour démontrer qu'une applet acceptée par le BCV ne provoquera pas d'erreur.