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


19/12/2005 : Le langage Hume et son modèle de coût
Armelle Bonenfant (University of St Andrews) Résumé

12/12/2005 : Intégration des modélisations 3D des sciences de la terre au sein d'environnements de la RV pilotés par grappe de PC
Souley Madougou (LIFO) Résumé
Attention : Attention 13h45 Amphi H

29/11/2005 : Evaluating Quantified Boolean Formulas
Marco Benedetti (ITC Trento) Résumé
Attention : Attention : mardi 14h (salle de réunion 1)

28/11/2005 : Représentation des langages de n-uplets d'arbres par des programmes logiques et applications
Sébastien Limet (LIFO) Résumé
Attention : 14h - Amphi H

21/11/2005 : Simulations de biomolécules: le rôle du parallélisme et de la réalité virtuelle
Marc Baaden (CNRS Laboratoire de biochimie théorique) Résumé

17/10/2005 : Complexité de Kolmogorov et calcul des ressemblances.
Jean-Paul Delahaye (LIFL (Lille)) Résumé
Attention : 13h45 Amphi Herbrand

17/10/2005 : Traces
Pierre Deransard (INRIA Rocquencourt) Résumé
Attention : 15h15 Amphi Herbrand

03/10/2005 : Visualisation haute performance pour calcul scientifique intensif
Jean-Philippe Nominé (CEA) Résumé

26/09/2005 : Apprentissage de solveurs de contraintes sur les domaines finis
Andrei Legtchenko (LIFO) Résumé
Attention : Soutenance de thèse à 13h45 amphi Herbrand

19/09/2005 : Présentation de MAC OS
Sylvie Haouy Maure (LIFO) Résumé

12/09/2005 : à venir
Gaël Dias (université de Beira interior (Covilha, Portugal)) Résumé

27/06/2005 : Study of the parallelization of the continuous global optimization with constraints by using interval analysis
Benyoub Abdeljalil (University of Cadi Ayya (Marrakesh)) Résumé

20/06/2005 : Functional Modelling of Interactive Systems
Walter Dosch (Université de Luebeck) Résumé

13/06/2005 : Reconstruction 3D d'objets par une représentation fonctionnelle
Christophe Rosenberger (LVR (Bourges)) Résumé

06/06/2005 : Contrainte d'inclusion dans les données semi-structurées
Denis Debarbieux (Lille (LIFL)) Résumé

25/04/2005 : Programmation fonctionnelle d'ordinateurs parallèles et de méta-ordinateurs : sémantiques, systèmes et preuves
Frédéric Loulergue (Paris) Résumé

25/04/2005 : Méta-politiques de sécurité pour les réseaux à grande échelle
Patrice Clémente (ENSI Bourges) Résumé
Attention : 2ieme séminaire donc à 16h

11/04/2005 : Contributions à l'algorithmique de la vérification
Jean Michel Couvreur (Bordeaux) Résumé

11/04/2005 : Réservation de ressources pour les groupes d'utilisateurs : compromis entre qualité et coûts.
Christian Laforest (Université d'Evry) Résumé
Attention : 2ième séminaire donc à 16h

04/04/2005 : Controlling Salinity in a Potable Water Supply System Using a Constraint Programming Approach
Jimmy Ho-Man Lee (Université chinoise de Hong Kong) Résumé

04/04/2005 : Algorithme évolutionnaire pour sélectionner les meilleurs complexes protéine-protéine
Jérôme Azé (LRI Université Paris Sud) Résumé
Attention : 2ième séminaire donc à 16h

29/03/2005 : Résolution parallèle de problèmes irréguliers : de la mémoire partagée à la grille de calcul
Michael Krajecki (Université de Reims) Résumé
Attention : Exceptionnellement le mardi à 11h

21/03/2005 : Analyse d'accessibilité dans les systèmes de réécriture pour la vérification de protocoles cryptographiques.
Thomas Genet (IRISA) Résumé

14/03/2005 : Modèles et politiques de sécurité pour les systèmes d'information et de communication distribués et hétérogènes
Anas ABOU EL KALAM (ENSI Bourges) Résumé

07/03/2005 : Evaluation des performances de programmes parallèles haut niveau à base de squelettes algorithmiques
Anne Benoit (Edimbourg) Résumé

28/02/2005 : Verification and certification in knowledge processing
Areski Nait Abdallah (INRIA) Résumé

21/02/2005 : Les apports de la biologie en informatique: modèles de calcul bio-inspirés
Serghei Verlan (Université de Metz) Résumé

07/02/2005 : Aspects dynamiques des bases de données XML
Mirian Halfel (Université François Rabelais (Blois)) Résumé

24/01/2005 : Axiomatisation complète de la construction d'arbres sur un ensemble ordonné
Khalil Djelloul (LIFM (Marseille)) Résumé

17/01/2005 : Model-checking, Satisfiability and Expressiveness for the TQL Logic
Jean Marc Talbot (LIFL) Résumé


Résumés des séminaires


Le langage Hume et son modèle de coût Armelle Bonenfant, University of St Andrews

Hume (Higher-order Unified Meta-Environment) is a strongly typed, mostly-functional language with an integrated tool set for developing, proving and assessing concurrent, safety-critical systems. Hume aims to extend the frontiers of language design for resource-limited systems, including real-time embedded and safety-critical systems, by introducing new levels of abstraction and provability. The current issue is to provide a cost model for Hume consisting on time and space analysis, basically built after the hume abstract machine. I will present you the basics of the language and expose the current state of my research.


Intégration des modélisations 3D des sciences de la terre au sein d'environnements de la RV pilotés par grappe de PC Souley Madougou, LIFO

La visualisation scientifique joue un rôle fondamental dans l'interprétation des données scientifiques et techniques. Avec l'explosion de la taille des données consécutivement à l'évolution des instruments de mesure et d'acquisition de données, le stockage, la transmission et la visualisation de ces données sont devenus des problèmes difficiles. Diverses solutions allant des techniques d'optimisation graphique ou de stockage aux algorithmes complexes de multirésolution en passant par les techniques de rendu parallèle sont proposées. Pour être efficaces, certaines applications doivent combiner toutes ces solutions. C'est typiquement le cas de celles de réalité virtuelle. En effet, dans ce domaine, les algorithmes de rendu doivent s'adapter aux contraintes fortes et simultanées d'interaction temps-réel et d'immersion pour offrir un réalisme convaincant à l'utilisateur . Dans cette thèse, nous proposons une méthode parallèle de gestion interactive de grands volumes de données géoréférencées pour les environnements de réalité virtuelle pilotés par grappe de PC. Cette méthode combine les techniques sus-citées à un modèle de calcul parallèle classique. Un accent particulier est mis sur la multirésolution dépendante de la vue à cause non seulement de la navigation spécifique aux environnement de réalité virtuelle mais aussi du type d'objets manipulés qui sont de très grande étendue. Pour minimiser les coûts de communication, diverses techniques de compression sont proposées. Notre modèle est capable de rendre en temps réel, des modèles réputés difficiles à visualiser et est extensible à l'instar des grappes de PC pour lesquelles il est défini.


Evaluating Quantified Boolean Formulas Marco Benedetti, ITC Trento

SAT solvers are the most effective tools for solving important classes of industrial-scale problems (in computer-aided design of integrated circuits, planning, model checking, scheduling, cryptography, ...). For example, they have been successfully used in classical planning: Given a propositional theory describing (1) an initial (known) state, (2) a goal state, and (3) a set of possible (deterministic) actions, a SAT solver can be used to find a plan, i.e. a course of actions that achieves the goal. This is a "purely existential" problem, so long as we simply wonder whether or not a plan *exists* for the initial state. One step ahead of SAT solvers, we encounter QBF provers. They manage the language of QBFs (Quantified Boolean Formulas), which adds the quite valuable possibility to quantify universally over the truth value of variables (i.e. to require that some property holds for all the truth values of some variable). Such additional expressive power enlarges the scope of problems we can address. Also, it allows us to produce an exponentially succinct formulation for some of the "old" ones. Let us consider the following ?conformant? planning problem: "Given a set of possible initial states, find a plan that is guaranteed to work whichever the state we actually start from.?. The alternation of quantifiers now play a key role in stating that real question: ?Does a plan exist ? such that for all the initial states? the goal is achieved??. A QBF solver is required to deal with such a problem. But, are QBF solvers worthy of inheriting the amazing success of SAT solvers? Not yet. Several improvements over the state of the art are necessary for QBF solvers to face real-world cases. In this talk, we describe a new QBF solving paradigm designed to leverage the added value of universal quantifiers at solving time - a noticeable step towards real-world QBF solvers. The approach we present - called symbolic skolemization - is the first one to be expressly designed for QBFs, with no re-use or adaptation of techniques developed for SAT solvers. We also mention a number of additional techniques we introduced to complement our symbolic solver: quantifier-tree reconstruction, hybrid inference engine, SAT-based sub-solutions, model extraction, and formula certification, among the others. To conclude, a publically available system implementing this whole set of techniques - called "sKizzo" - is described, and experimental results and comparisons are discussed.


Représentation des langages de n-uplets d'arbres par des programmes logiques et applications Sébastien Limet, LIFO

Dans le domaine de l'informatique théorique, on manipule très souvent des relations sur les termes du 1er ordre. Par conséquent, il est important d'avoir des représentations finies de ces relations, encore appelées langages de n-uplets d'arbres. Nous avons étudié différentes représentations possibles pour une classe de langages appelée langages synchronisés. Nous avons plus particulièrement étudié une représentation sous forme de programmes logiques et présenté un algorithme basé sur les techniques de transformation de programmes pour calculer les opérations sur les langages. Dans ce cadre, nous avons montré des propriétés intéressantes des langages synchronisés et de certaines de leurs sous-classes. Puis, nous avons appliqué les résultats obtenus à des problèmes liés aux domaines de la démonstration automatique et de la vérification. Ces résultats s'appuient sur une procédure de construction d'un programme logique qui décrit la clôture réflexive transitive de la relation induite par un système de réécriture.


Simulations de biomolécules: le rôle du parallélisme et de la réalité virtuelle Marc Baaden, CNRS Laboratoire de biochimie théorique

Les simulations de systèmes moléculaires d'intérêt biologique sont aujourd'hui un outil indispensable pour la compréhension de processus à l'échelle atomique. A l'aide d'exemples concrets les différentes étapes d'un projet de simulation sont décrites. Le rôle du parallélisme dont l'utilisation est déjà bien implantée dans cette communauté scientifique est brièvement évoqué suivi de quelques applications actuelles de la réalité virtuelle dans ce domaine. La dernière partie sera consacrée à un projet dont le but est de faciliter et généraliser l'utilisation de la réalité virtuelle.


Complexité de Kolmogorov et calcul des ressemblances. Jean-Paul Delahaye, LIFL (Lille)

On présentera diverses idées mathématiques utilisées pour saisir la notion de ressemblance entre objets textuels ou situés dans un espace géométrique (par exemple le plan ou l'espace de dimension 3). De toutes les notions envisagées, la distance informationnelle (provenant de la théorie algorithmique de l'information de Kolmogorov) semble la plus générale. Elle est aussi susceptible d'applications intéressantes comme celles récemment proposées pour la classification automatique de textes, de séquences génétiques, de langues et d'images.


Traces Pierre Deransard, INRIA Rocquencourt

20 ans de recherche commune avec Gérard Ferrand et un peu plus


Visualisation haute performance pour calcul scientifique intensif Jean-Philippe Nominé, CEA

Les grands calculateurs parallèles pour le calcul scientifique autorisent des simulations de plus en plus poussées et détaillées de phénomènes physiques ou de systèmes technologiques complexes. La visualisation interactive des grands volumes de résultats de calcul qui en découlent doit suivre la cadence, sous peine de laisser se creuser l'écart entre capacités de calcul brutes et possibilités d'interprétation effective des simulations. Après avoir rappelé la démarche générale en visualisation scientifique et situé quelques ordres de grandeur et applications typiques, nous présenterons quelques-unes des approches développées au CEA/DIF (complexe de calcul du CEA à Bruyères-le-Châtel) : parallélisation des chaînes de traitements, notamment avec les logiciels EnSight et la plateforme "open source" VTK, utilisation de grappes de PC, amélioration de l'interaction 3D.


Apprentissage de solveurs de contraintes sur les domaines finis Andrei Legtchenko, LIFO

La programmation par contraintes est un outil très puissant de modélisation et de résolution de problèmes. Un problème est modélisé par un ensemble de variables et un ensemble de contraintes sur ces variables. Les solutions sont ensuite trouvées par un système appelé solveur de contraintes. Un solveur est un logiciel complexe souvent basé sur des subtiles propriétés des contraintes. Un solveur peut être représenté par un algorithme de recherche combiné avec un algorithme d?itération d?opérateurs de réduction de domaines. Afin de faciliter la construction d?opérateurs de réduction, il est envisageable de les dériver automatiquement à partir des contraintes du problème. <> Dans cette étude nous proposons un cadre général et plusieurs techniques pour la construction automatique d?opérateurs de réduction à partir de la spécification en extension d?une contrainte (par une table de solutions). Les techniques se repartissent en deux catégories, selon la nature de la contrainte : - le cas d?une contrainte classique où toutes les solutions sont connues. En utilisant des techniques issues de l?apprentissage automatique, on propose d?exploiter les régularités du nuage de solutions afin de produire des opérateurs ayant une grande puissance de réduction et un coût d?exécution réduit. - le cas d?une contrainte partiellement définie où seuls des exemples de solutions et de non-solutions sont connus. Dans ce cas la contrainte est d?abord apprise sur les exemples sous la forme d?une fonction de satisfiabilité exprimée dans un langage donné. Ensuite les opérateurs de réduction sont dérivés à partir de cette fonction en utilisant le procédé de l?extension aux ensembles. Une nouvelle méthode d?apprentissage supervisé de classificateurs, inspirée par la forme générale de propagateurs, a également été proposée.


Présentation de MAC OS Sylvie Haouy Maure, LIFO


à venir Gaël Dias, université de Beira interior (Covilha, Portugal)

à venir


Study of the parallelization of the continuous global optimization with constraints by using interval analysis Benyoub Abdeljalil, University of Cadi Ayya (Marrakesh)

1 Scientific and economic tallies 1.1 Where are the needs for intensive calculation? The definition of intensive calculation uses the computing power necessary to run an application. The computing power is the quantity of calculation (number of elementary operations) used per unit of time. Indeed, an application can have to answer time constraints or resources. A relatively modest quantity of calculation that should be done in reduced time can require a great computing power. A scientific application will be considered intensive if its code must be strongly optimized to use as well as possible the resources of computing available and to respect the time constraints. Many are the examples of intensive applications: modelling of the climate, the simulation of nuclear explosions, aeronautics, the human genome, linear algebra, operations research, optimization, .... etc. The introduction of parallelism, in the technology of design of processors and of the information processing systems, is justified by the requirement needed in computing power and consumption for memory capacity. 1.2 Machines able to meet these needs Architecture of the computers dedicated to intensive computing such as defined above evolutes quickly. One can distinguish four great classes from machines adapted to various applications types: -Supercomputers (vectorial and parallel architectures). -Clusters (federation of di®erent architectures: PCs, SUN machines,Macs, ...., etc). -Distributed systems and grids of computing. -Systems on silicon (or System one Chip, SoC). 2 Framework of this seminar We will be interested in the study, on a parallel architecture with distributed memories, of parallelization of Hansens algorithm: a sequential algorithm of Branch-and-Bound type developed for the resolution of the problem of global optimization with inequality constraints. Due to the fact that this algorithm is dynamic and irregular, we propose parallel algorithms based on the load balancing in terms of quantity and quality of the boxes. Our developed techniques are based on the use of "the best first strategy". Simulations carried out show the importance of the integration of load balancing in order to improve quality of the parallel codes. Parallel codes are based on PROFILE/BIAS libraries for the management of interval analysis, C++ and MPI environment for the management of communications between processors of the parallel architecture. Key-words: Parallelism, global optimization, Branch-and-Bound methods, load balancing, interval analysis.


Functional Modelling of Interactive Systems Walter Dosch, Université de Luebeck

Interactive systems are composed of software and hardware components of different types that exchange information along connecting channels. The functional modelling, systematic design and correct implementation of interactive systems needs sound foundations for describing the interface and the behaviour of communicating components. The stream-based approach models the input/output behaviour of a component as a function between communication histories. The lecture addresses the foundations of untimed component-based systems with asynchronous communication. On the specification level, we concentrate on the component's input/output behaviour. For the systematic design, we present compositional techniques for the stepwise refinement. On the implementation level, we discuss the systematic introduction of control states and data states into behavioural specifications. We understand states as abstractions of communication histories and present a formal method for systematically transforming a stream function into a state-based implementation.


Reconstruction 3D d'objets par une représentation fonctionnelle Christophe Rosenberger, LVR (Bourges)

Ce séminaire présente des travaux sur la reconstruction 3D dans le cadre de la thèse de pierre-alain fayolle doctorant au LIFO et actuellement au Japon. La reconstruction 3D a de nombreuses applications : réalité virtuelle, préservation du patrimoine culturel (art, lieux historiques) et industrie. Le contexte de travail est la reconstruction d?objets en 3 dimensions à partir d'un nuage de points sur la surface de l'objet obtenu typiquement à l'aide d'un scanner laser 3D. L?originalité de l?approche proposée consiste à représenter cet objet par une fonction mathématique (modèle FREP). Cette approche permet d'une part de représenter un objet par une quantité d'information très faible (fonctions mathématiques et paramètres) et facilite d'autre part, les transformations des objets crées (déformation, zoom,..). Un des enjeux de notre travail est la détermination du modèle FREP et des paramètres associés à un ensemble de points sur la surface de l'objet. Nous avons utilisé des algorithmes génétiques afin de réaliser cette tâche.


Contrainte d'inclusion dans les données semi-structurées Denis Debarbieux, Lille (LIFL)

Une donnée semi-structurée est modélisée par un graphe étiqueté à plusieurs racines. Le but de cet exposé est d'étudier les contraintes d'inclusion sur ces graphes. La contrainte d'inclusion 'p est inclus dans q' est satisfaite par un graphe si tout noeud accessible par la requête régulière p est aussi accessible par la requête q. Dans cet exposé, trois problèmes sont abordés: 1) Un nouvel algorithme pour le problème de l'implication d'une contrainte 'p est inclus dans q' par un ensemble de contraintes bornées est présenté. Cet algorithme améliore les résultats de S.Abiteboul, V.Vianu, ou N.Alechina et al. donnés dans un cadre plus général. Si les contraintes se réduisent à des équivalences entre mots, on propose un algorithme qui améliore celui de P.Buneman et al. 2) La notion de modèle exact est introduite: un document D est un modèle exact d'un ensemble de contraintes C si une contrainte d'inclusion est satisfaite par D si et seulement si elle est impliquée par C. On prouve que tout ensemble de contraintes a un modèle exact et on se pose la question de l'existence des modèles exacts finis. 3) On étudie enfin, s'il est possible d'optimiser des requêtes régulières en utilisant des contraintes d'inclusion. Dans ce cas, le problème est de calculer, à partir d'un ensemble de contraintes C et d'une requête q, une requête finie q équivalente à p par rapport à C.


Programmation fonctionnelle d'ordinateurs parallèles et de méta-ordinateurs : sémantiques, systèmes et preuves Frédéric Loulergue, Paris

De nombreux problèmes comme la simulation de phénomènes physiques ou la manipulation de bases de données de grandes tailles nécessitent des performances que seuls les ordinateurs massivement parallèles, voire les méta-ordinateurs, peuvent fournir. Nous présenterons un aperçu de nos travaux sur la programmation parallèle de haut niveau qui facilite leur usage. Notre méthode a été de partir d'un modèle de parallélisme structuré possèdant un modèle de prévision de performances (Bulk Synchronous Parallel ou BSP) puis de concevoir un ensemble d'opérations universelles qui permet la programmation de n'importe quel algorithme de ce modèle. Une approche opérationnelle nous a amené à définir des extensions du lambda-calcul par des primitives BSP. Une bibliothèque basée sur ces calculs, la bibliothèque BSML a été développée pour le langage fonctionnel Objective Caml. La programmation BSML s'appuie sur une structure de données parallèle polymorphe. Les programmes sont des fonctions Objective Caml usuelles mais manipulent cette structure de données parallèle à l'aide d'un petit ensemble d'opérations dédiées. BSML suit le modèle BSP et est donc garanti sans inter-blocage. La confluence des calculs garantit quant à elle le déterminisme de BSML. La prévision de performances selon le modèle BSP a été vérifiée. Un nouvel axe de recherche, toujours dans la conception de langages, est d'avoir un langage pour le metacomputing, c'est-à-dire pour la programmation de grappes de machines parallèles (qui sont elles-mêmes souvent des grappes de PC) que nous appelons méta-ordinateurs. Pour cela nous avons combiné le langage BSML, pour la programmation de chaque noeud parallèle, et notre nouveau langage MSPML (Minimally Synchronous Parallel ML) pour la coordination de l'ensemble. MSPML diffère de BSML par l'absence de barrières de synchronisation globale. À chaque fois ces extensions et ces nouveaux langages sont basés sur une sémantique formelle et un modèle de prévision de performances associé est donné. Plus récemment nous avons entrepris des travaux sur la certification tant des programmes BSML eux-mêmes que de la compilation et des machines d'exécution destinées à ces programmes.


Méta-politiques de sécurité pour les réseaux à grande échelle Patrice Clémente, ENSI Bourges

Je présenterai mes travaux de recherche menés à l?ENSI de Bourges. Ces travaux s?inscrivent dans les activités de recherche en sécurité menées depuis trois ans par les membres du LIFO localisés à l'ENSI de Bourges ou au CEA DAM, sous l?égide de C. Toinard. La thématique de ces travaux est la sécurité dans les réseaux à grande échelle, au sein desquels les n?uds sont potentiellement hétérogènes (OS différents, restrictions spécifiques, etc.) La sécurité dans les réseaux à large échelle est un problème complexe qui met en jeu de nombreux facteurs et nécessite une expertise souvent accrue sur chacun des systèmes. De plus, l?administration des systèmes sécurisés pose parfois de sérieux problèmes car les outils mis à disposition sont trop complexes ou trop fins. L?une des ambitions ici est de proposer des méthodes et outils facilitant l?administration de réseaux à grande échelle. L'approche choisie est l'utilisation d'un méta-langage de définition de politiques de sécurité. Les méta-politiques définies à l?aide de ce langage ont vocation à être diffusées sur tous les n?uds du réseau pour une traduction respectant le système d?exploitation local, les outils de sécurité, ainsi que certaines contraintes et restrictions physiques et/ou administratives. Nous avons travaillé (avec les étudiants que j?ai encadré) sur la définition d?un méta-langage commun à au moins deux systèmes d?exploitation « de confiance » : SE Linux et GR Security. Je présenterai les grandes lignes de ce méta-langage, en mettant en relief les intersections et les différences les deux systèmes cibles. Je présenterai également les limites actuelles du méta-langage, inhérentes à ces différences. Je présenterai enfin rapidement les deux outils de traduction du méta-langage vers les deux systèmes cibles que nous avons conçus. Je préciserai le travail restant à faire et terminerai par les nombreuses perspectives de ces travaux et notamment leur poursuite cette année, pour aboutir notamment à des outils de traduction ascendants, ainsi que l?apport pour la thèse de Jeremy Briffaut, en détection d?intrusion.


Contributions à l'algorithmique de la vérification Jean Michel Couvreur, Bordeaux

A venir


Réservation de ressources pour les groupes d'utilisateurs : compromis entre qualité et coûts. Christian Laforest, Université d'Evry

Les communications entre membres d'un même groupe d'utilisateur se généralise avec les réunions sur réseau, les video conférences, les forums, les jeux sur réseau, etc. Ces applications réclament une grande qualité de transmission des informations. Une façon d'essayer d'atteindre cela est de réserver des ressources qui seront exclusivement dédiées au groupe. Il faut alors atteindre le meilleur équilibre entre la qualité de la structure réservée et son coût. Cet exposé s'interessera aux aspects algorithmiques de cette réservation de ressources. De manière plus précise, je présenterai dans un premier temps un algorithme permettant de donner simultanément des garanties sur un critère de qualité ET sur le critère de coût (il s'agit d'un algorithme d'approximation multi-critères). Dans un deuxième temps je présenterai un algorithme permettant de maintenir des garanties sur la qualité tout en prenant en compte le caractère évolutif ("dynamique") d'un groupe d'utilisateurs : les membres d'un groupe peuvent arriver dans un ordre quelconque, à des instants très différents, etc... Il s'agit ici d'un travail sur les algorithmes onlines ou algorithmes incrémentaux. Pour terminer j'évoquerai rapidement d'autres travaux que j'ai menés, relatifs aux groupes d'utilisateurs : partage des coûts, réservation de ressources d'un lien multi-canaux (ordonnancements). Contrairement à de nombreuses études mon approche n'est pas expérimentale mais analytique (preuves des rapports obtenus).


Controlling Salinity in a Potable Water Supply System Using a Constraint Programming Approach Jimmy Ho-Man Lee, Université chinoise de Hong Kong

Salinity is the concentration of salts in water. The raw water system of a China city relies on water from a river for potable use. The water source is located close to the interface between sea water and fresh river water. During the dry winter months, the river water level recedes and the sea water intrudes into the river streams, causing drastic rises in the salinity of the fresh water in the system. This salinity period affects the daily lives of some 450,000 residents of the city. The raw water system consists of three pumping stations and four reservoirs, which are all stocked up with fresh water of low salinity at the beginning of the salinity period. During the salinity period, salinity of the river source fluctuates immensely as affected by tidal activities and weather conditions. Based on prediction of the daily salinity patterns at the water source, our task is to optimize the logistical operations, such as how many pumps to operate and how much water to transfer among reservoirs, so as (1) to satisfy the daily water consumption requirement of the city and (2) to keep the potable salinity below a desirable level targeted by the local Water Department for as many days as possible. We adopt a constraint programming approach to the problem. In this talk, we give a detailed description of the problem in addition to discussing the modeling issues as well as the search heuristics employed. Our system is under final user testing and will be deployed for water management operations and experimentation with different salinity scenarios. The project is in collaboration with the International Institute for Software Technology, United Nations University.


Algorithme évolutionnaire pour sélectionner les meilleurs complexes protéine-protéine Jérôme Azé, LRI Université Paris Sud

La fonction de la plupart des protéines est subordonnée à l'interaction avec un ou plusieurs partenaires, qui peuvent être aussi bien de petites molécules que des macromolécules. Les complexes protéine-protéine sont impliqués dans beaucoup de processus cellulaires et physiologiques, c'est pourquoi ils présentent un grand intérêt dans l'étude des fonctions cellulaires et biochimiques de leurs composants. A l'heure actuelle, alors que les projets de génomique structurale fournissent un accés de plus en plus large aux structures des protéines isolées, on sait encore peu de choses sur leur assemblage. Les procédés employés pour déterminer la structure des protéines isolées sont difficilement applicables pour la détection des structures des complexes car ces derniers peuvent être instables d'un point de vue temporel et énergétique. De plus, le nombre de conformations possibles est trop élevé pour permettre une étude exhaustive de toutes les conformations candidates. L'objectif des projets de génomique structurale est d'obtenir des informations structurales sur un très grand nombre de protéine, de manière rapide et systématique. Celles-ci sont ensuite intégrées dans une approche fonctionnelle. Sachant que la durée moyenne pour obtenir la structure d'une protéine isolée est de l'ordre de 6 mois, l'analyse systématique de complexes implique la mise en oeuvre de solutions informatiques validées expérimentalement si besoin. Les algorithmes permettant d'engendrer les conformations candidates à partir de structures de protéines isolées sont appelés des "algorithmes de docking". Ces algorithmes engendrent un ensemble de conformations candidates et sélectionnent les meilleurs selon des critères énergétiques, géométriques ou autres. L'objectif du travail réalisé en collaboration avec l'IBBMC ( Institut de Biochimie et de Bio-physique Moléculaire et Cellulaire) d'Orsay est de définir une stratégie de post-élagage des conformations candidates fournies par l'algorithme de docking. Cet élagage est réalisé grâce à une fonction de score apprise à partir de conformations annotées comme étant des complexes avérés ou non. L'apprentissage est réalisé par un algorithme évolutionnaire, ROGER, qui optimise un ensemble de fonctions en utilisant le critère de l'aire sous la courbe ROC (Receiver Operating Characteristic).


Résolution parallèle de problèmes irréguliers : de la mémoire partagée à la grille de calcul Michael Krajecki, Université de Reims

Cet exposé sera organisé en trois parties. Dans un premier temps, je me concentrerai sur la résolution en mémoire partagée des problèmes de satisfaction de contraintes (CSP, constraint satisfaction problems, en anglais). Cette modélisation de haut niveau m'a permis d'étudier et de valider principalement deux méthodes de résolution parallèle basées, d'une part sur l'élimination de variables, et d'autre part, sur la décomposition des domaines du CSP initial. Je présenterai également quelques résultats préliminaires sur le problème de car sequencing. L'optimisation combinatoire est un prolongement des travaux que j'ai menés sur les CSP en me rapprochant du monde industriel. Les problèmes d'ordonnancement industriel ne peuvent être résolus en temps polynomial par des algorithmes exacts de nature séquentielle ou parallèle. Les métaheuristiques représentent alors des alternatives intéressantes pour la résolution de ce type de problèmes. L'intérêt dans le calcul parallèle est à deux niveaux : une amélioration supplémentaire de la qualité des solutions obtenues ainsi qu'un temps de calcul réduit. Au cours de cette deuxième partie, je présenterai une approche parallèle d'optimisation par colonies de fourmis dans ce contexte. Enfin, j'introduirai l'intergiciel CONFIIT qui est destiné à permettre l'exécution complètement distribuée d'une application sur une grille de calcul. Cet intergiciel s'appuie sur l'ensemble des résultats que j'ai obtenus par ailleurs : décomposition de domaine pour dégager du parallélisme, technique d'équilibrage de charge adaptée, et exploitation de la programmation par échange de messages et en mémoire partagée. Je montrerai en particulier comment CONFIIT peut être utilisée pour la résolution de CSP et de problèmes en optimisation combinatoire (application au problème de Langford).


Analyse d'accessibilité dans les systèmes de réécriture pour la vérification de protocoles cryptographiques. Thomas Genet, IRISA

Dans cet exposé, je ferai un état des lieux de la technique de calculs de descendants (ou termes accessibles) dans les systèmes de réécriture que nous développons et de ses applications. Je présenterais d'abord la technique principale est un algorithme générique de complétion des automates d'arbre qui permet de calculer de façon exacte (quand c'est possible) ou approchée (dans le cas contraire) l'ensemble des descendants. Cet algorithme est implanté dans l'outil Timbuk (http://www.irisa.fr/lande/genet/timbuk/). Ensuite, nous verrons comment utiliser le calcul des descendants pour vérifier des programmes et des systèmes infinis modélisés par des systèmes de réécriture. Nous verrons qu'à l'aide du calcul de descendants, il est possible aussi bien de montrer l'accessibilité que la non accessibilité d'une configuration du système modélisé. Ceci est appliqué à la vérification de protocoles cryptographiques, où les configurations sont représentées par des termes et le protocole et le comportement de l'intrus sont modélisés par des systèmes de réécriture. La vérfication d'un protocole consiste ensuite en la preuve que les configurations représentant des attaques ne font pas partie des configurations atteignables (i.e. des descendants). A ce niveau, nous verrons également l'intérêt, tant théorique que pratique, du calcul approché. Enfin, je donnerai les pistes sur lesquelles nous travaillons afin d'améliorer la technique et les nouvelles applications qui se dégagent en vérification.


Modèles et politiques de sécurité pour les systèmes d'information et de communication distribués et hétérogènes Anas ABOU EL KALAM, ENSI Bourges

Nous commençons par proposer une démarche méthodologique pour définir des politiques de sécurité adaptées aux systèmes d?informations et de communication en santé et social (SICSS). Ces systèmes couvrent l?ensemble des besoins généralement trouvés dans les autres domaines : interopérabilité des systèmes, complexité des organisations, sensibilité des informations et diversité des exigences de sécurité (confidentialité, intégrité, disponibilité et auditabilité). Le but de la méthode présentée est de réaliser un bon compromis entre le respect du principe du moindre privilège et la flexibilité du contrôle d?accès. La première étape consiste à décrire le système, identifier les informations à protéger et caractériser les menaces. La politique de sécurité vient ensuite spécifier comment contrer ces menaces, en exprimant d?une part, un ensemble de propriétés de sécurité qui doivent être satisfaites, et d?autre part, un ensemble de règles permettant de modifier l?état de protection du système. Les politiques de sécurité que nous proposons ont l?originalité de tenir compte du contexte et de l?interopérabilité, et d?être suffisamment souples pour prendre en compte toute amélioration, changement ou mise à jour dans le système. Par ailleurs, un nouveau modèle de contrôle d'accès sera présenté : le modèle Or-BAC (pour Organization-Based Access Control). Ce modèle permet de prendre en compte des informations de contexte dans l?expression des règles, afin de spécifier un contrôle d?accès fin et adapté. Il est aussi un moyen de spécifier, dans un cadre homogène, plusieurs politiques de sécurité pour des organisations différentes devant coopérer. Or-BAC n?est pas restreint aux permissions, mais permet également de définir des interdictions, des obligations et des recommandations. À cet égard, Or-BAC est capable de spécifier des politiques de sécurité pour les SICSS, comme il peut être appliqué à une gamme très large d?applications complexes, interopérables et distribuées. Or-BAC est d?abord représenté par des diagrammes UML, puis dans un nouveau langage logique fondé sur la logique déontique. Il est par ailleurs intégré dans une modélisation UML d?une démarche sécuritaire globale spécifiant les aspects statiques et dynamiques des phases d?authentification et d?autorisation., et allant de l'analyse des besoins jusqu'aux implémentation par des mécanismes de contrôles d'accès, en intégrant une politique des sécurité. Enfin, sera présenté un prototype montrant ces différentes étapes et réalisant un contrôle d'accès dans un environnement distribué et hétérogène.


Evaluation des performances de programmes parallèles haut niveau à base de squelettes algorithmiques Anne Benoit, Edimbourg

Dans un contexte de programmation pour les grilles de calcul (ensemble hétérogène de ressources reliées par un réseau, accessible à une communauté d'utilisateurs), la programmation à base de squelettes algorithmiques exploite le fait que de nombreuses applications utilisent les mêmes schémas de programmation bien connus. Cette approche de haut niveau permet ainsi de structurer aisément les programmes parallèles en fournissant à l'utilisateur une librairie de squelettes (routines génériques) prédéfinis. Dans le projet eSkel -- Edinburgh Skeleton Library (http://homepages.inf.ed.ac.uk/abenoit1/eSkel), motivés par nos observations sur les précédentes tentatives pour implémenter ces idées, nous avons commencé à définir un ensemble générique de squelettes sous la forme d'une librairie de fonctions C, basée sur MPI. La première partie du séminaire présentera la librairie eSkel, en présentant les principaux concepts fondamentaux à la base de la librairie. L'utilisation d'un squelette donné de la librairie eSkel implique de nombreuses informations sur les dépendances imposées sur le scheduling de l'application. La deuxième partie du séminaire montre comment nous exploitons cette information dans le projet Enhance (http://groups.inf.ed.ac.uk/enhance), en modélisant les squelettes à l'aide d'algèbres de processus. Nous pensons pouvoir obtenir ainsi des résultats permettant de prendre de meilleures décisions d'ordonnancement sur la grille que les approches moins sophistiquées. De plus, les techniques développées sur les grilles permettent d'obtenir les performances des ressources utilisées de façon dynamique, ce qui permet un réordonnancement dynamique de l'application.


Verification and certification in knowledge processing Areski Nait Abdallah, INRIA

One of the major applications of the Curry-Howard isomorphism is the production of machine-checkable certificates of correctness for functional programs. We examine the extension of this paradigm to knowledge processing, in particular in the case where only partial or tentative knowledge is available. Our approach also covers the utilization of non-monotonic frameworks for commonsense reasoning.


Les apports de la biologie en informatique: modèles de calcul bio-inspirés Serghei Verlan, Université de Metz

Certaines opérations en biologie moléculaire, notamment les manipulations d'ADN, peuvent être vues comme des transformations d'information. Il est donc naturel de les considérer de ce point de vue et de rechercher des modèles de calculs fondés sur ces opérations. Le résultat est étonnant: dans la plupart des cas les modèles obtenus sont très puissants et ils ont la puissance d'expression d'une machine de Turing. Les systèmes de Head et leurs extensions, fondés sur l'opération de la recombinaison, sont des modèles parmi les plus importants dans le domaine. Nous allons présenter pas à pas les réflexions nécessaires pour arriver de l'opération biologique à l'opération de la recombinaison et les systèmes de Head. Nous allons montrer comment des structures de contrôle permettent d'augmenter la puissance d'expression et nous présenterons l'état de l'art. À la fin nous présenterons éventuellement quelques autres opérations bio-inspirés, ainsi que les notions de base des systèmes à membranes, inspirés par la structure et le fonctionnement de la cellule vivante.


Aspects dynamiques des bases de données XML Mirian Halfel, Université François Rabelais (Blois)

Le langage XML est un standard pour l'échange d'information via Internet. Dans ce cadre, en général, les documents XML doivent être valides, c'est-à-dire, ils doivent respecter un ensemble de contraintes donné. Nous étudions la validation des documents XML par rapport aux contraintes de schéma (structure) et les contraintes d'intégrité (clés et clés étrangères). Nous considérons des mises-à-jour sur un document XML valide et nous proposons des méthodes pour effectuer sa validation de façon incrémentale, c'est-à-dire, en vérifiant seulement la partie du document concernée par les mises-à-jour. Nous utilisons les automates d'arbre pour tester de façon incrémentale la validité d'un document et nous proposons différentes approches pour le cas des mises-à-jour ne respectant pas les contraintes. En particulier, nous considérons le cas des mises-à-jour qui déclenchent l'évolution des schémas.


Axiomatisation complète de la construction d'arbres sur un ensemble ordonné Khalil Djelloul, LIFM (Marseille)

Notre travail porte sur la structure (un ensemble muni d'opérations et de relations) des arbres aux feuilles ordonnées qui est un mélange des arbres munis d'opérations de construction et d'un ordre dense sans extrêmes portant sur les feuilles de ces arbres. Nous axiomatisons cette structure par une théorie du premier ordre, c'est-à-dire un ensemble de propositions du premier ordre. Pour montrer la complétude de la théorie nous utilisons un théorème général que nous établissons préalablement. Ce théorème fait intervenir un quantificateur nouveau, affirmant essentiellement l'existence d'une infinité d'individus ayant une propriété du premier ordre donnée. De notre démonstration de complétude il est possible d'extraire les grandes lignes d'une procédure de décision pour cette théorie.


Model-checking, Satisfiability and Expressiveness for the TQL Logic Jean Marc Talbot, LIFL

We study the TQL logic introduced by Cardelli and Ghelli. The TQL logic, inspired from the ambient logic, is the core of a query language for semistructured data represented as unranked and unordered trees. We will address three issues for this logic: first, we investigate the complexity of model-checking, ie deciding whether a tree is a model of a formula. Then, we study the satisfiability problem for this logic (ie deciding whether a given formula admits a model) as well as its expressiveness; in particular, we will compare various fragments of the TQL logic with the monadic second-order logic.