• 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)

14/12/2009 : Analyse syntaxique du français : constituants et dépendances
Benoît Crabbé (Paris 7) Résumé

09/12/2009 : Séminaire des doctorants SDS
Organisé par Jonathan Rouzaud-Cornabas (ENSI Bourges) Résumé
Attention : ENSI-Bourges (Salle E210) de 15h à 18h.

07/12/2009 : Comment se rencontrer de manière asynchrone dans un graphe quelconque
Arnaud Labourel (LABRI) Résumé

23/11/2009 : Vérification de propriétés régulières et temporelles pour des programmes Java.
Benoit Boyer (IRISA Rennes) Résumé
Attention : 15H

16/11/2009 : From Model-Checking to Temporal Logic Constraint Solving
Aurélien Rizk (INRIA Rocq) Résumé
Attention : 15H

16/11/2009 : Defining reliable services coordinations for accessing data in dynamic environments
Genoveva Vargas (Franco Mexican Laboratory of Informatics and Automatic Control) Résumé
Attention : 16H

09/11/2009 : Modèles de graphe aléatoire à classes chevauchantes pour l’analyse des réseaux
Pierre Latouche (Laboratoire Statistique et Génome - Evry) Résumé

02/11/2009 : -
Journée des doctrants (-) Résumé

26/10/2009 : Algorithmic Randomness: A Prime
Cristian S. Calude (The University of Auckland ) Résumé

19/10/2009 : Machines à signaux et modèles de calcul analogiques
Jerome Durand Lose (LIFO) Résumé Slides

06/07/2009 : How fast can you 2-approximate the bandwidth of a graph?
Serge Gaspers (LIRMM Montpellier ) Résumé

25/05/2009 : Cryptographic Protocol Analysis: Looking Inside the Black Box
Christopher Lynch (Univ. de Potsdam, NY) Résumé
Attention : Salle SR1

18/05/2009 : Classification de données multi-sources par la théorie des fonctions de croyance
Arnaud Martin (ENSIETA Brest) Résumé

20/04/2009 : Analyse syntaxique relâchée à base de contraintes
Jean-Philippe Prost (LIFO) Résumé

20/04/2009 : Interaction Homme-Machine Multimodale: Concepts, Modèles, Outils et Applications
Yacine Bellik (Laboratoire d'Informatique pour la Mécanique et les Sciences de l'Ingénieur (Paris)) Résumé
Attention : 15H

06/04/2009 : Un environnement pour le développement de grammaires à portée sémantique
Yannick Parmentier (LORIA ) Résumé

06/04/2009 : Parallélisation de traitements de flux sur des systèmes embarqués
Julien BERNARD (ENSIMAG) Résumé
Attention : 15H

30/03/2009 : La logique programmable pour le calcul haute performance
Olivier Trémois (-) Résumé

23/03/2009 : A Certified Data Race Analysis for a Java-like Language
Frederic Dabrowski (INRIA Rennes) Résumé

16/03/2009 : Largeur de rang et quelques applications en étiquetage de graphes
Mamadou Kante (Labri Bordeaux) Résumé

09/03/2009 : Contributions à la Modélisation des Réseaux Complexes : Prétopologie et Applications
Vincent Levorato (Laboratoire d'Informatique et des Systemes Complexes de l'Ecole Pratique des Hautes Etudes) Résumé
Attention : A 15H après le séminaire de 14h

09/03/2009 : Algorithmes de type EM pour l'estimation des modèles de mélange multivariés semi- et non-paramétriques
Didier Chauveau (MAPMO Orléans) Résumé

02/03/2009 : Géométrie pour l'aute-assemblage
Florent Becker (ENS Lyon) Résumé

23/02/2009 : Calcul quantique par mesure
Simon Perdrix (LFCS, University of Edinburgh & PPS, Université Paris Diderot) Résumé

23/02/2009 : Programmation générative & Architecture parallèle : Vers une méthodologie pour la génération systématique d'outils de développement
Joel Falcou (LRI Paris XI) Résumé
Attention : A 15H et d'une durée de 2H

16/02/2009 : Alignement de structures secondaires d'ARN
Claire Herrbach (LIFO) Résumé
Attention : A 15H après le séminaire de 14h

02/02/2009 : La mobilité : une autre approche logicielle
Fabrice Mourlin (LACL Paris 12) Résumé

26/01/2009 : Simulation du ruissellement d'eau de pluie sur des surfaces agricoles.
Olivier Delestre (MAPMO) Résumé

26/01/2009 : Un environnement pour la preuve et la programmation
Matthieu Sozeau (LRI Paris) Résumé
Attention : Séminaire des doctorants : 15 H

12/01/2009 : The Infinity Computer and Numerical Calculus
Yaroslav D. Sergeyev (Italie) Résumé

05/01/2009 : Sémantiques formelles pour un compilateur certifié du langage C
Sandrine Blazy (INRIA Rocquencourt) Résumé

Résumés des séminaires

Analyse syntaxique du français : constituants et dépendances Benoît Crabbé , Paris 7
Je présenterai une technique d'analyse syntaxique statistique pour la langue naturelle à la fois en constituants et en dépendances. L'analyse procède en ajoutant des étiquettes fonctionnelles aux sorties d'un analyseur en constituants, entraîné sur le French Treebank, pour permettre l'extraction de dépendances typées. D'une part, nous spécifions d'un point de vue formel et linguistique les structures de dépendances à produire, ainsi que la procédure de conversion du corpus en constituants (le French Treebank) vers un corpus cible annoté en dépendances, et partiellement validé. D'autre part, nous décrivons l'approche algorithmique qui permet de réaliser automatiquement le typage des dépendances. En particulier, nous nous focalisons sur les méthodes d'apprentissage discriminantes d'étiquetage en fonctions grammaticales.

Séminaire des doctorants SDS Organisé par Jonathan Rouzaud-Cornabas, ENSI Bourges
Intervenant: Nicolas Greneche
Directeur de Thèse: P. Berthomé
Sujet: Des propriété de sécurité sur un système distribuée: Application à un cluster sous Linux.
Résumé: Un langage a été défini permettant d'exprimer les propriétés de sécurité requises pour un système au moyen de la notion de séquence d?appels système et d?opérateurs entre séquences. Ces propriétés peuvent être garanties en calculant des chemins dans des graphes d'interactions. Il s'agit de compléter les travaux menés et en cours, en les élargissant aux systèmes répartis. En effet, actuellement nous savons exprimer des propriétés pour un système mais pas à l?échelle d?un système réparti. L?idée est d?offrir un langage adapté à un système réparti afin d?exprimer des propriétés de sécurité complexes prenant en compte des séquences d?opérations qui sont réparties sur plusieurs machines.

Intervenant: Xavier Kauffman
Directeur de Thèse: P. Berthomé
Sujet: Des propriété de sécurité sur un système distribuée: Application à un cluster sous Linux.
Résumé: 1. Présentation du contexte - - Cifre - - Entreprise 2. Présentation du sujet de la thèse - - Attaques sur carte à puces - - Modélisation et simulation 3. Domaines et techniques impactés

Intervenant: Jonathan Rouzaud-Cornabas
Directeur de Thèse: C. Toinard
Sujet: Prévenir des ruptures de propriétés de sécurité sur unsystème d'exploitation : une approche basée sur la dépendance causale Résumé:Les propriétés de sécurité permettent d'exprimer des faits qui doivent toujours être valables sur le système pour que ce dernier garde un bon niveau de sécurité. Les propriétés de sécurité sont de type /intégrité/, /confidentialité/ ou /disponibité/. Dans cet exposé, je parlerai de la propriété de non-interference et une nouvelle manière de la représenter pour les OS. Pour cela, j'introduirai un langage d'expression de propriétés de sécurité et une preuve du fonctionnement de la propriété de non-interference. Je présenterai l'architecture et l'implémentation des propriétés de sécurité sur un système d'exploitation classique (Linux). Je reviendrai sur les performances ainsi que sur l'efficacité de mon implémentation.

Comment se rencontrer de manière asynchrone dans un graphe quelconque Arnaud Labourel, LABRI
Dans cet exposé, je montrerais comment deux agents mobiles peuvent se rencontrer dans un graphe quelconque et possiblement infini. Le graphe est inconnu des agents et ses sommets sont anonymes. À chaque étape, l'agent doit choisir un numéro de port correspondant à une des arêtes incidentes du sommet courant et traverser cette arête. Les deux agents se rencontrent s'ils sont sur un même sommet ou s'ils se croisent sur une arête. On considère le modèle asynchrone. C'est-à-dire que la durée de chaque étape d'un agent est déterminée par un adversaire omniscient qui essaye d'empêcher le rendez-vous. Les agents ont des identifiants uniques afin de permettre le rendez-vous de manière déterministe. En effet, sans identifiants, deux agents déterministes auraient le même comportement et ne se rencontreraient jamais dans un cycle. Je montrerais que le rendez-vous est toujours possible dans les graphes sous ces conditions et comment étendre ce résultat au rendez-vous d'agents mobiles dans le plan.

Vérification de propriétés régulières et temporelles pour des programmes Java. Benoit Boyer, IRISA Rennes
Il parfaitement connu que le problème d'atteignabilité en réécriture est un problème indécidable. Malgré tout, plusieurs techniques permettent de résoudre une instance du problème en calculant une sur-approximation de l'ensemble des termes atteignables. Ainsi la complétion d'automates d'arbres[FGT'04] permet de calculer une sur-approximation régulière de l'ensemble des termes atteignables pour un système de réécriture donné à partir d'un ensemble régulier de termes initiaux. Cette technique s'adapte particulièrement bien à la vérification de protocoles cryptographiques mais aussi à la vérification de programmes Java [BGJLR'07]. Dans ce dernier cas, il serait cependant intéressant de vérifier des propriétés plus fines en introduisant une notion de temporalité. C'est l'objet de cet exposé : montrer comment introduire une relation d'ordre entre les termes atteignables dans un automates d'arbres, et comment exploiter cette relation pour vérifier des propriétés temporelles sur des programmes Java. [FGT'04] : G. Feuillade, T. Genet and V. Viet Triem Tong. Reachability Analysis of Term Rewriting Systems [BGJLR'07] : Y. Boichut, T. Genet, T. Jensen and L. Le Roux. Rewriting Approximations for Fast Prototyping of Static Analyzers

From Model-Checking to Temporal Logic Constraint Solving Aurélien Rizk, INRIA Rocq
We show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain D, and by computing a validity domain for the variables rather than a truth value for the formula. This makes it possible to define a continuous degree of satisfaction for a temporal logic formula in a given system, as well as distances between structures w.r.t.~a formula, opening up the field of model-checking to optimization. We illustrate this approach with reverse-engineering problems originating from systems biology, for searching parameter values in high dimensions, and for estimating the robustness of a system w.r.t.~temporal logic specifications.

Defining reliable services coordinations for accessing data in dynamic environments Genoveva Vargas, Franco Mexican Laboratory of Informatics and Automatic Control
The emergence of ubiquitous computing introduces wireless and portable technologies that democratize access to information and services and thereby opens new research challenges for middleware and services brokering techniques that can cope with this novel dynamic execution environment. Research on services oriented middleware and on autonomic computing is important and promising for supporting the execution and deployment of current and future ambient systems. The characteristics of ambient systems define new requirements to the accessibility and interaction capabilities of all the environments where people travel, walk, work and live. From the middleware point of view the challenges include transparent access to data and ressources by coordinating services that give transparent access to sensors, devices, networks, and processes. The resulting services coordination is a long running process that consumes and produces data and that must be reliable, (i.e., exception tolerant, secure) and adaptable according to its execution environment. In this talk I will introduce the notion of services coordinations focussing on the data access problem within dynamic environments consisting of heterogeneous devices with different physical capacities that provide data and computing capabilities for data intensive applications. I will highlight the main challenges concerning this proble and I will also introduce an approach for addressing them.

GENOVEVA VARGAS-SOLAR is deputy director the Franco-Mexican Laboratory of Informatics and Automatic Control (LAFMIA UMI 3175). She is senior researcher of the French Council of Scientific Research (CNRS) and she is member of the HADAS group of the Informatics Laboratory of Grenoble, France. She also is senior researcher of the Data and Knowledge Management Group of the Research Centre of Information and Automation Technologies at Universidad de las Americas Puebla. She is elected president of the Mexican Society of Computer Science. In 2000, she obtained her first PhD degree in Computer Science at University Joseph Fourier and in 2005 she obtained her second PhD degree in Literature at University Stendhal. In 1997 she obtained her first Master Degree in Computer Science at University Joseph Fourier and in 1998 she obtained her second Master Degree in Compared Literature at University Stendhal. She did her undergraduate studies on Computer Systems Engineering at Universidad de las Americas in Puebla. Her research interests in Computer Science concern distributed and heterogeneous databases, reflexive systems and service based database systems. Her research interests in Literature concern middle age Literature, myths’ critics and myths’ analysis applied to different myths of origins. She has coordinated several research projects in Europe and Latin America financed by governments and industrial partners. She actively promotes the scientific cooperation in Computer Science between Latin America and Europe particularly between France and Mexico.

Modèles de graphe aléatoire à classes chevauchantes pour l’analyse des réseaux Pierre Latouche, Laboratoire Statistique et Génome - Evry
Les réseaux sont largement utilisés dans de nombreux domaines scienti?ques a?n de représenter les intéractions entre objets d’intérêt. Ainsi, en biologie, les réseaux de régulation s’appliquent à décrire les mécanismes de régulation des gènes, à partir de facteurs de trans- cription, tandis que les réseaux métaboliques permettent de représenter des voies de réactions biochimiques. En sciences sociales, ils sont couramment utilisés pour réprésenter les intérac- tions entre individus. Dans ce contexte, de nombreuses méthodes non-supervisées de clustering ont été développées a?n d’extraire des informations, à partir de la topologie des réseaux. La plupart d’entre elles partitionne les noeuds dans des classes disjointes, en fonction de leurs pro- ?ls de connection. Récemment, des études ont mis en évidence les limites de ces techniques. En effet, elles ont montré qu’un grand nombre de réseaux “réels” contenaient des noeuds connus pour appartenir à plusieurs groupes simultanément. Pour répondre à ce problème, nous pro- posons l’Overlapping Stochastic Block Model (OSBM). Cette approche autorise les noeuds à appartenir à plus d’une classe et généralise le très connu Stochastic Block Model, sous cer- taines hypothèses. Nous montrons que le modèle est identi?able dans des classes d’équivalence et nous proposons un algorithme d’inférence basé sur des techniques variationnelles globales et locales. Finalement, en utilisant des données simulées et réelles, nous comparons nos travaux avec d’autres approches.

- Journée des doctrants, -
le programme de la journée ainsi que les résumés des différentes présentations. http://univ-orleans.fr/lifo/evenements/JDDL09

Algorithmic Randomness: A Prime Cristian S. Calude, The University of Auckland
Measuring and calibrating incompressibility is used to define algorithmically random objects, finite (e.g. bit strings) or infinite (e.g. reals). The talk presents theoretical and experimental recent results that shed new lights on Monte Carlo simulations, mathematical provability and quantum randomness.

Machines à signaux et modèles de calcul analogiques Jerome Durand Lose, LIFO
Après une présentation des machines à signaux, nous poseront la question de savoir ce qu'est un nombre réel. À cette question nous proposerons deux réponses qui mènent à deux mondes différents : - - représentation exacte et approche semi-algébrique : le modèle de Blum, Shub et Smale - - approximation de plus en plus fine : l'analyse récursive (machines de Turing de type 2) Nous montrons ensuite comment ces deux approches peuvent être implantées avec des machines à signaux et une utilisation judicieuse de points d'accumulation.

How fast can you 2-approximate the bandwidth of a graph? Serge Gaspers, LIRMM Montpellier
This talk is based on joint work with Martin Fürer (Pennsylvania State University) and Shiva Prasad Kasiviswanathan (Los Alamos National Laboratory). The bandwidth of a graph G on n vertices is the minimum b such that the vertices of G can be labeled from 1 to n such that the labels of every two adjacent vertices differ by at most b. In this talk, I will present a 2-approximation algorithm for the Bandwidth problem that takes worst-case O(1.9797^n) = O(3^{0.6217 n}) time. This improves the previous best O*(3^n) time bound (the O* notation is similar to the usual big-Oh notation except that factors polynomial in n are ignored) for the same approximation ratio and the previous best 3-approximation algorithm of Cygan and Pilipczuk (Proceedings of ICALP 2009, to appear), which runs in time O*(2^n). The algorithm decomposes the vertex set of G into ordered sets (called buckets) of (almost) equal sizes such that all edges are either between vertices in the same bucket or adjacent buckets. The idea is to find the smallest bucket size for which there exists such a bucket arrangement. The algorithm relies on a divide-and-conquer strategy, on dynamic programming and on the enumeration of vertex subsets and connected components of a graph.

Cryptographic Protocol Analysis: Looking Inside the Black Box Christopher Lynch , Univ. de Potsdam, NY
Cryptographic Protocols often have subtle bugs that are discovered years after the protocols are in use. Therefore, it is important to analyze the correctness of protocols. They are generally analyzed in two different ways. One way is to analyze by hand, arguing mathematically about the algorithm used for encryption. A second method is to analyze the protocols by computer, with the encryption algorithm considered as a black box. The first method has the disadvantage that it is not automated, and humans often miss possible attacks. In this talk we argue in favor of the second method, by proposing a fully automatic approach for analyzing protocols using Horn Clauses, in combination with equational theories to describe the properties of the encryption algorithm, that leads to a better analysis.

Classification de données multi-sources par la théorie des fonctions de croyance Arnaud Martin, ENSIETA Brest
La caractérisation en environnement incertain nécessite généralement plusieurs capteurs ou plusieurs observations sous des angles différents. Les approches de fusion d’information permettent de combiner ces informations multiples. Les imperfections des capteurs et des traitements doivent être prises en compte lors de fusion d’informations. Face aux imperfections des données, plusieurs approches sont possibles : i) les supprimer, ii) développer des algorithmes robustes à ces imperfections, iii) les modéliser. Les théories de l’incertain prennent le partie de modéliser au mieux ces imperfections pour en tenir compte jusqu’à la décision finale. Plusieurs approches de fusion permettent une telle modélisation. On s’attachera ici à positionner la théorie des fonctions de croyance par rapport à la théorie des probabilités et à présenter sa richesse et ses intérêts de manière simple. Nous reviendrons en particulier sur les derniers opérateurs de combinaison permettant de gérer le conflit - problème inhérent à la combinaison de différentes sources d’informations - et nous verrons également comment décider sur des informations conflictuelles.

Analyse syntaxique relâchée à base de contraintes Jean-Philippe Prost, LIFO
La syntaxe modèle-théorique (Model-Theoretic Syntax, ou MTS) fait référence à une famille de cadres formels qui permettent une étude de la syntaxe basée sur la théorie des modèles. En ceci, elle se différencie notablement des cadres dédiés à la syntaxe dite générative-énumérative (Generative-Enumerative Syntax, ou GES), qui découlent de la théorie de la preuve. Les conséquences sur l'étude et le traitement de la langue sont significatives, notamment pour la représentation de phénomènes linguistiques non pris en compte par la GES tels que l'ouverture lexicale (création permanente de nouveaux termes), les fragments bien formés (e.g. "Il me semble que...", "Oui, mais alors je...", etc.), l'agrammaticalité, ou encore la grammaticalité graduelle (i.e. gradience). Au cours de ce séminaire, je présenterai un algorithme d'analyse syntaxique pour le formalisme MTS des Grammaires de Propriétés. Je m'attacherai tout particulièrement à souligner le traitement de l'agrammaticalité et de la gradience.

Interaction Homme-Machine Multimodale: Concepts, Modèles, Outils et Applications Yacine Bellik, Laboratoire d'Informatique pour la Mécanique et les Sciences de l'Ingénieur (Paris)
Nos travaux prennent place dans le domaine de l'interaction Homme-Machine et plus particulièrement dans celui de l'interaction multimodale. Ils concernent l'analyse, la conception, le développement et l'évaluation de systèmes interactifs disposant de différents moyens d'interaction et dépassant le cadre classique des interfaces graphiques. Les récentes évolutions technologiques et sociales (avènement de la société de l'information, mobilité des utilisateurs en situation d'interaction, apparition de l'informatique ambiante,…) créent de nouveaux besoins en termes d'interaction. La diversité des utilisateurs, des systèmes et des environnements fait qu'il n'est plus possible de continuer à proposer des interfaces au comportement prédéfini et figé. Face à ce problème nous adoptons une approche qui consiste à intégrer dans le système interactif des mécanismes d'adaptation qui vont lui permettre de modifier dynamiquement son comportement pour être en adéquation avec un contexte d'interaction en perpétuelle évolution. La diversité des interactions qu'offrent les interfaces multimodales, leur flexibilité et leur caractère intuitif et naturel, les rendent aptes à cibler différentes catégories d'utilisateurs, à s'accommoder des fréquentes modifications que peut subir l'environnement physique de l'interaction et à exploiter de façon optimale les dispositifs physiques des systèmes qui les accueillent. Nous cherchons dans mes travaux à élaborer des modèles et des outils logiciels qui permettent d'exploiter de façon "intelligente" toutes les modalités dont peut disposer le système à un instant donné pour interagir avec l'utilisateur. Nous commencerons par introduire les concepts relatifs à la multimodalité puis nous décrirons les modèles et les outils développés dans nos travaux. Nous illustrerons notre présentation avec des exemples d'applications multimodales développées à l'aide de ces outils. Notre présentation sera structurée en 2 volets. Le premier traitera des problèmes liés à la multimodalité en entrée (de l'utilisateur vers le système). Le second sera consacré aux problèmes posés par la multimodalité en sortie (du système vers l'utilisateur). Nous conclurons par des perspectives relatives aux travaux déjà effectués mais également à de nouvelles thématiques à explorer.

Un environnement pour le développement de grammaires à portée sémantique Yannick Parmentier, LORIA
Disposer de ressources linguistiques intégrant non seulement des informations sur la structure syntaxique d'un énoncé, mais également sur le sens de cet énoncé peut être intéressant pour de nombreuses applications telles que Traduction Automatique, Systèmes de Dialogue, Systèmes de Question-Réponse, etc. Cependant le coût de développement de telles ressources est important, d'où l'intérêt de disposer d'outils adaptés. Dans cet exposé, nous présentons un environnement logiciel open source permettant (i) de décrire des grammaires à portée sémantique, et (ii) d'utiliser les grammaires ainsi décrites pour l'analyse syntaxique et le calcul d'une représentation du sens d'un énoncé. Bien qu'utilisé principalement pour le développement de grammaires d'arbres (grammaires d'arbres adjoints, grammaires d'arbres adjoints multi-composantes, grammaires d'interaction), cet environnement repose sur une architecture modulaire, favorisant une extension à d'autres formalismes grammaticaux. Cet environnement est utilisé actuellement pour le développement de grammaires noyaux du francais, de l'anglais, de l'allemand, du coréen, et également dans le cadre d'un système de dialogue (jeu d'aventure textuel).

Parallélisation de traitements de flux sur des systèmes embarqués Julien BERNARD, ENSIMAG
Les systèmes embarqués possèdent de plus en plus de ressources de calculs et doivent assurer de plus en plus de fonctions. Nous présentons un algorithme adaptatif basé sur du vol de travail permettant de paralléliser des traitements de flux et nous montrons une implémentation dans le cas d'un traitement d'image sur la plateforme Traviata de STMicroelectronics (lecteur DVD).

La logique programmable pour le calcul haute performance Olivier Trémois, -
Depuis sa création en 1984, le FPGA (composant de logique programmable) est vu généralement comme une petite entité utile pour interfacer différents composants numérique (logique de glue). Toutefois, depuis plus de 10 ans, des multiplieurs embarqués permettent aux FPGA d’intervenir dans des processus de calcul haute performance : calculs financiers, recherche pétrolière, imagerie médicale, cryptographie, météorologie, … La fréquence de fonctionnement des FPGA est faible (300-400 MHz) comparée à la fréquence de référence des processeurs INTEL ou AMD (3 GHz) ou des DSP (1GHz), mais les plus gros FPGA ont entre 1000 et 2000 multiplieurs embarqués qui peuvent travailler en parallèle, de concert avec des dizaines de milliers de tables de vérités (LUT : Look-Up Table) et de registres. Au cours de ce séminaire, une petite introduction sur le FPGA vous permettra de mieux appréhender ce composant, les méthodes de programmation seront ensuite abordées, finalement, l’utilisation des FPGAs en imagerie médicale et la présentation d’une plateforme de calcul haute performance viendront clore cet exposé.

A Certified Data Race Analysis for a Java-like Language Frederic Dabrowski, INRIA Rennes
Nous nous intéressons à l'interprétation abstraite de programmes JAVA "multithreadés". Une première étape consiste à définir la sémantique de tels programmes. La sémantique "interleaving", généralement considérée, est une approximation incorrecte du modèle mémoire (description des comportements admissibles) de JAVA. Cependant, ce dernier assure (Data Race Free Guarantee) que cette sémantique est correcte pour les programmes bien synchronisés (race free). Nous présentons une analyse statique, certifiée en COQ, qui permet de garantir qu'un programme JAVA est bien synchronisé. Cette analyse est basée sur la proposition de Naik et Aiken (POPL2007), pour un langage "While", qu'elle généralise à un sous ensemble significatif de JAVA.

Largeur de rang et quelques applications en étiquetage de graphes Mamadou Kante, Labri Bordeaux
En algorithmique distribuée, il est important que l'information soit distribuée entre les sommets du réseau. Pour des contraintes d'espace on ne peut pas toujours stocker toute l'information dans les noeuds. Il faut alors trouver une représentation compacte du réseau: chaque noeud a une partie de l'information. Nous nous intéressons aux classes de graphes qui ont une largeur de clique localement bornée, i.e., des classes de graphes qui sont des "recollements" de classes de graphes qui ont une largeur de clique bornée. Nous allons montrer que si G est dans une classe de graphes de largeur de clique localement bornée et P une propriété du premier ordre alors on peut stocker des informations de taille logarithmique sur chaque noeud et tester si G vérifie P en utilisant seulement ces informations.

Contributions à la Modélisation des Réseaux Complexes : Prétopologie et Applications Vincent Levorato , Laboratoire d'Informatique et des Systemes Complexes de l'Ecole Pratique des Hautes Etudes
Un réseau complexe est un réseau d'interactions entre entités dont on ne peut pas déduire le comportement global à partir des comportements individuels desdites entités, d'où l'émergence de nouvelles propriétés. Notre problème est l'analyse et la modélisation de ces réseaux. L’analyse nécessite un formalisme englobant à la fois structure (approche statique) et fonction (approche dynamique), afin d'avoir une meilleure compréhension des caractéristiques de ces réseaux. En premier lieu, nous présenterons rapidement les modélisations utilisées jusqu'à présent et basées sur la théorie des graphes, sensées simuler le comportement des réseaux complexes. En analysant les faiblesses de ces modèles quant à une représentation convaincante des réseaux du monde réel (réseaux sociaux, informatiques, biologiques, ...), nous apporterons une définition formelle générale d'un réseau par le biais de la théorie de la prétopologie, laquelle permet d'exprimer au mieux la dynamique de ces systèmes. En second lieu, nous proposerons de nouveaux algorithmes d'analyse basés sur la classification d'éléments et la recherche d'éléments centraux, afin de fournir des outils d'aide à la décision puissants. Enfin nous présenterons une librairie logicielle associée à des structures de données permettant la mise en oeuvre de simulations efficaces de tout modèle basé sur la théorie de la prétopologie. Mots clés: Prétopologie, Algorithmique, Réseaux Complexes, Classification, Centralité, PretopoLib

Algorithmes de type EM pour l'estimation des modèles de mélange multivariés semi- et non-paramétriques Didier Chauveau, MAPMO Orléans
Nous présentons un nouvel algorithme pour l'estimation des modèles de mélange finis, dans lesquels les observations sont multidimensionnelles de coordonnées indépendantes conditionnellement à leur sous-population de provenance, mais de distributions nonparamétriques, c'est-à-dire non restreintes à des familles paramétriques de lois, ce qui permet des modélisations plus libres. Cet algorithme est une généralisation d'un algorithme introduit récemment par Bordes, Chauveau, & Vandekerkhove (2007), pour des mélanges univariés de densités symétriques. Nous présentons quelques résultats récents sur l'identifiabilité de tels modèles, et montrons en quoi cet algorithme et ses différentes déclinaisons sont plus efficaces que d'autres méthodes d'estimation pour ces modèles. Différentes versions de cet algorithme sont implémentées dans le package mixtools pour le logiciel de statistiques R, avec lequel sont effectués les simulations et exemples sur des données réelles.

Géométrie pour l'aute-assemblage Florent Becker, ENS Lyon
Afin de modéliser l'assemblage de nano-structures d'ADN, des bio-informatictiens autour de Ned Seeman et Erik Winfree ont mis au point le modèle des "pavages auto-assemblants". Dans ce modèle, à mi-chemin entre pavages du plan et automates cellulaires, des particules carrées interagissent en s'agrégeant ou non suivant leurs affinités pour former des structures "intéressantes". Ce modèle est à la fois très simple à définir, et relativement fidèle aux résultats expérimentaux. Dans un premier temps, le travail sur ce modèle a consisté à montrer son universalité (toute forme est auto-assemblable), et à trouver des mécanismes de résistance aux erreurs. Dans cet exposé, je montrerai comment une approche géométrique, fondée sur des "systèmes de signaux" permet de résoudre trois autres défis: trouver des systèmes les plus simples possibles, rendre l'assemblage plus rapide, et donner une manière plus naturelle de spécifier l'auto-assemblage, c'est à dire une forme de langage de programmation pour l'auto-assemblage.

Calcul quantique par mesure Simon Perdrix, LFCS, University of Edinburgh & PPS, Université Paris Diderot
Le calcul quantique par mesure, introduit par Briegel et Raussendorf, est non seulement une des plus prometteuses propositions de réalisation physique de l'ordinateur quantique, mais ouvre aussi de nouvelles perspectives théoriques, notamment en terme de parallélisation des opérations quantiques. La mesure, brique de base de ce modèle, a une évolution fondamentalement probabiliste. Aussi l'existence d'une évolution globalement déterministe dépend de l'état initial du calcul qui est représenté par un graphe. Nous montrons que l'existence d'un flot généralisé dans ce graphe est une condition nécessaire et suffisante à l'existence d'une exécution globalement déterministe. De plus, nous introduisons un algorithme classique efficace permettant de décider si un graphe donné admet un flot généralisé. Enfin, nous montrons que le pouvoir computationnel du calcul par mesure est le même que celui des circuits quantiques avec fan-out non borné. On en déduit que la transformée de Fourier quantique peut être approximée en profondeur constante dans le cadre du calcul quantique par mesure, et que la factorisation peut être approximée par un algorithme classique probabiliste polynomial incluant des appels à du calcul quantique par mesure de profondeur constante.

Programmation générative & Architecture parallèle : Vers une méthodologie pour la génération systématique d'outils de développement Joel Falcou, LRI Paris XI
Les besoins croissants en puissance de calcul exprimés par de nombreux domaines scientifiques exercent une pression très forte sur les architectures émergentes, les rendant toujours plus performantes mais toujours plus complexes à maîtriser. Dans ce cadre, le développement d'outils tirant partie des spécificités de ces architectures ( quadri et bientôt octo-coeurs, processeur Cell ou GPU par exemple) devient une gageure car allier expressivité et efficacité devient une tâche ardue. De nombreux travaux visant à utiliser des techniques comme la programmation générative en général et la métaprogrammation en particulier ont démontré leur pertinence mais peu de méthodologie claire n'en émerge. Nous nous proposons ici de définir une telle méthodologie et de montrer comment elle a permis le développement d'outils de parallélisation automatique dans le domaine du traitement d'image et du signal pour des architectures aussi variées que les machines multi-coeurs, les clusters ou le processeur Cell.

Alignement de structures secondaires d'ARN Claire Herrbach, LIFO
Nos travaux portent sur la comparaison de structures secondaires d'ARN sans pseudo-noeud. Il est possible de modéliser ces structures par des arbres ordonnés étiquetés. Il existe des algorithmes polynomiaux d'édition et d'alignement d'arbres (Zhang-Shasha 89, Jiang et al. 95). Cependant,les opérations d'éditions utilisées par ces algorithmes ne sont pas adaptées pour l'ARN. D'un autre côté, il a été montré que si l'on utilise un jeu d'opérations réaliste d'un point de vue biologique, le problème de l'édition de structures secondaires sans pseudo-noeud est NP-complet (Blin et al. 03). Nous avons étudié le problème de l'alignement, avec ce même jeu d'opérations réaliste, de structures secondaires d'ARN sans pseudo-noeud. Nous présenterons un algorithme polynomial pour ce problème, ainsi qu'une étude de la complexité en moyenne de cet algorithme et de l'algorithme d'alignement d'arbres de Jiang et al.

La mobilité : une autre approche logicielle Fabrice Mourlin, LACL Paris 12
La mobilité d'action au sein d'un logiciel est une voie d'évolution pour obtenir un logiciel plus réactif en particulier à son contexte d'exécution. Les travaux de recherche présentés dans ce document explore cette notion suivant trois aspects. Une première facette est la spécification de la mobilité au travers de langages formels tel que le pi calcul d'ordre supérieur. Les spécifications obtenues représentent des supports d'analyse essentiels. Ils offrent des possibilités de génération d'informations importantes telles que des tests ou du code exécutable. Ainsi, la réalisation ou la mise en œuvre de la mobilité est la deuxième facette de ce travail, où il est davantage question de construction à partir de spécifications formelles. Les implémentations fournies ont alors un objectif essentiel de validation de propriétés. Enfin le dernier aspect abordé porte sur l'architecture des applications à base d'agents mobiles. La définition d'une structure logicielle commune exprime la volonté de réutiliser l'expérience acquise dans des domaines d'intérêt différents. Nous avons fait le choix d'aborder le domaine de la surveillance logicielle, des serveurs d'agents mobiles et enfin du calcul numérique. Si les idées maîtresses sont partagées, chaque domaine impose ses propres spécificités qui entraînent une adaptation de la réalisation. Mots clés : spécification formelle, agent mobile, surveillance logicielle, calcul numérique.

Simulation du ruissellement d'eau de pluie sur des surfaces agricoles. Olivier Delestre, MAPMO
Dans le cadre d'un projet ANR : METHODE, nous nous intéressons à la simulation du ruissellement d'eau de pluie sur des surfaces agricoles. Pour cela, nous utilisons le système de Saint-Venant. Celui est résolu numériquement par une méthode aux volumes finis dite well-balanced. Nous avons développé un code C++ basée sur cette méthode : FullSWOF. Ce code est en phase de validation sur un ensemble de solutions exactes et de données expérimentales produites par L'INRA d'Orléans à "petites" échelles. Comme l'objectif est de simuler à l'échelle de bassin versant, la parallélisation du code est fortement envisagée.

Un environnement pour la preuve et la programmation Matthieu Sozeau, LRI Paris
Coq est un assistant de preuve basé sur la théorie des types permettant la vérification de développements mathématiques variés comme le théorème des quatre couleurs ou le théorème fondamental de l'arithmétique mais aussi informatiques comme la vérification d'un compilateur ou d'une librairie de calcul sur les grands entiers. Ce succès est dû non seulement à une logique très riche mais surtout à la possibilité dans ce formalisme de mélanger preuves et programmes, allant jusqu'à unifier la preuve de théorèmes et la vérification de programmes. Coq inclus donc en son sein un langage purement fonctionnel servant à la fois à la spécification, la programmation et la représentation des preuves. Je présenterais ce langage et son système de types qui inclus des types dépendants permettant d'énoncer des spécifications très précises. Ces types dépendants posent de nouveaux problèmes dans leur intégration à un système de programmation. J'esquisserai les solutions développées dans ma thèse pour rationaliser leur utilisation et démontrerai leur intérêt sur des exemples.

The Infinity Computer and Numerical Calculus Yaroslav D. Sergeyev, Italie
Traditional computers execute arithmetical operations with finite numbers. The lecture introduces a new positional system with infinite radix allowing one to write down finite, infinite, and infinitesimal numbers as particular cases of a unique framework. The new numeral system gives possibility to introduce a new type of a computer – the Infinity Computer – able to operate not only with finite numbers but also with infinite and infinitesimal ones (the European Patent Office has expressed its positive opinion with respect to the patent). The new approach has a strong applied character and is not related to the non-standard analysis. It both gives possibilities to execute calculations of a new type and simplifies fields of mathematics where usage of the infinity and/or infinitesimals is necessary (e.g., divergent series, limits, derivatives, integrals, measure theory, probability theory, etc.). Applications that can be treated by computers are determined by their computational abilities. In the following there are listed both operations that the Infinity Computer can execute and traditional computers are not able to perform and some of new areas of applications. It becomes possible: to introduce notions of numbers of elements for infinite sets in a way compatible with the notion used traditionally for finite sets significantly evolving traditional approaches able to distinguish numerable sets from continuum only (the principle “The part is less than the whole” is used for this purpose); to substitute symbols +? and -? by spaces of positive and negative infinite numbers, to represent them in the memory of the Infinity Computer and to execute arithmetical operations with all of them using this new type of a computer, as we are used to do with usual finite numbers on traditional computers; to substitute qualitative descriptions of the type ‘a number tends to zero’ by precise infinitesimal numbers, to represent them in the memory of the Infinity Computer, and to execute arithmetical operations with them using the Infinity Computer as we are used to do with usual finite numbers using traditional computers; to calculate divergent limits and series, providing as results explicitly written different infinite numbers, to be possibly used in further calculations on the Infinity Computer; to calculate indeterminate forms (e.g., difference and division of divergent series) that can give as results different infinitesimal, finite or infinite numbers; to calculate on the Infinity Computer sums of divergent series and improper integrals of various types that can give as results different explicitly written infinite numbers; to evaluate functions and their derivatives at infinitesimal, finite, and infinite points (infinite and infinitesimal values of functions and their derivatives can be also explicitly calculated); to study divergent processes at different infinite points; to introduce notions of lengths, areas, and volumes of fractal objects obtained after infinite numbers of steps and compatible with traditional lengths, areas, and volumes of non-fractal objects and to calculate them in a unique framework. The Infinity Calculator using the Infinity Computer technology is presented during the talk. Additional information can be downloaded from the page http://www.thethe Infinitycomputer.com. Plus d'infos sur : https://www.univ-orleans.fr/lifo/Manifestations/NMC09/Abstracts/O_SERGEYEV_Yaroslav.html

Sémantiques formelles pour un compilateur certifié du langage C Sandrine Blazy, INRIA Rocquencourt
Dans cet exposé, je présenterai succinctement un compilateur optimisant du langage C appelé CompCert, ayant été formellement vérifié avec l'assistant à la preuve Coq. Je détaillerai en particulier la sémantique du principal langage intermédiaire du compilateur, qui a été définie selon différents styles de sémantique, ainsi que le modèle mémoire du compilateur. Enfin, j'expliquerai comment ces travaux ont été réutilisés pour construire un environnement dédié à la preuve de programmes en logique de séparation.