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

Lifo > LIFO seminars (french)

 Site en Français



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)


Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024

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


21/11/2011 : Histoire de l'informatique en France : une discipline controversée, une industrie bousculée
Pierre Mounier-Kuhn (CNRS & Université Paris-Sorbonne) Résumé

08/11/2011 : Soutenance de thèse : Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels
Julien Tesson (LIFO) Résumé
Attention : Débute à 13 h 45. Lieu : Apmhithéâtre Herbrand, bâtiment 3IA

10/10/2011 : Accessibilité numérique
Dominique Archambault (Université Pierre et Marie CURIE ) Résumé

04/07/2011 : Web sémantique : données liées et sémantique des schémas
Fabien Gandon (INRIA Sophia Antipolis ) Résumé

20/06/2011 : Etat de l'art de la virtualisation du poste de travail", suivie d'une petite démo.
Naly Raliravaka (Département d'informatique de l'université d'Orléans) Résumé

23/05/2011 : Computing under Vagueness
Apostolos SYROPOULOS (Greek Molecular Computing Group) Résumé

20/05/2011 : Analyse statique du noyau de XEN avec l'outil Frama-C. Retour d'expérience.
Nikolai Kosmatov (CEA Saclay) Résumé
Attention : Débute à 10 h 30.

16/05/2011 : Deciphering complex molecular systems: a new ambition for computer science and visualization
Matthieu Chavent (CEA - DIF Arpajon) Résumé

18/04/2011 : Bioniformatics, finding protein patterns in genoms
FOROUGHMAND ARAABI Mohammad Hadi (University of Tehran) Résumé

11/04/2011 : L'inférence grammaticale : du coeur de la discipline aux applications
Jean-Christophe Janodet (Machine Learning Research Team - Laboratoire Hubert Curien-St Etienne) Résumé

04/04/2011 : Construction des automates Büchi pour le model checking LTL, verifié en Isabelle/HOL
Jan Smaus (Research Group Foundations of Artificial Intelligence - Freiburg) Résumé

28/03/2011 : Sur l'énumération des arbres enrichis
Daniele Gardy (Prism Versailles ) Résumé

21/03/2011 : Unconventional Architectures: The Art of Programming Self-Organization
René Doursat (Ecole polytechnique - CNRS ) Résumé

14/03/2011 : Analyse de la complexité des algorithmes d'apprentissage relationnel
Aomar Osmani (Laboratoire D'informatique de Paris nord-LIPN ) Résumé

07/03/2011 : Constraint-Based Scheduling for Steel Production
Guido Tack (Department of Computer Science - K.U. Leuven) Résumé

21/02/2011 : Indécidabilité, pavages et polyominos
Nicolas Ollinger (LIF Marseille) Résumé

14/02/2011 : Logiques modales avec comptage
Guillaume Hoffmann (laboratoire LORIA, Université Henri Poincaré, Nancy) Résumé

07/02/2011 : Algorithmes de chiffrement/déchiffrement basé chaos pour la sécurité des images transmises.
Abir Awad (LIFO) Résumé

31/01/2011 : Toponym Disambiguation in Geographical Information Retrieval
Davide Buscaldi (LIFO) Résumé

24/01/2011 : Update XML Views
Jixue Liu (School of Computer and Information Science, University of South Australia) Résumé

10/01/2011 : ATI Tablette graphique
Sophie Robert et Mathieu Liedloff (LIFO) Résumé

03/01/2011 :
Réunion de département (Dpt Informatique - UFR Sciences) Résumé


Résumés des séminaires


Histoire de l'informatique en France : une discipline controversée, une industrie bousculée Pierre Mounier-Kuhn , CNRS & Université Paris-Sorbonne

Pourquoi la France, où l’on prétendait en 1947 avoir « une avance théorique » en calcul électronique, a-t-elle dû vingt ans après lancer un Plan Calcul pour rattraper son retard ? En dépouillant archives et revues scientifiques, on découvre que la France est le seul pays industrialisé où la recherche publique n’a pas réussi à construire d’ordinateur dans la période pionnière, avant 1960. L’informatique s’y est cependant développée grâce aux initiatives d’universitaires, véritables entrepreneurs de science, souvent en Province, qui collaboraient avec des industriels novateurs et avec les administrations techniques civiles ou militaires. Ils ont dû bientôt faire face à l’explosion de la demande du marché du travail, qui réclamait toujours plus d’informaticiens. Au cours des années 1960-1970, on est passé progressivement du calcul électronique, outil au service des ingénieurs et des mathématiques appliquées, à une discipline nouvelle, l’informatique, qui recomposait le paysage scientifique. Cette évolution ne s’est pas accomplie sans résistances et polémiques. D'autant qu'elle se situait dans le contexte des vicissitudes de l'industrie informatique et des politiques gouvernementales.


Soutenance de thèse : Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels Julien Tesson, LIFO

Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels. Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d’ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme - et l’assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l’extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, rai- sonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles. Nous prouvons ainsi la correction d’une implanta- tion du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d’applications partant d’une spécification d’un problème sous forme d’un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l’exécuter sur des machines parallèles.


Accessibilité numérique Dominique Archambault, Université Pierre et Marie CURIE

Le besoin d’accessibilité progresse, lentement, dans nos sociétés, et de nombreux progrès ont été faits dans différents domaines (bâtiment, urbanisme, etc.). Dans la société numérique, les “nouvelles” Technologies de l’Information et de la Communication portent en elles l’espoir de progrès formidables en matière d’accessibilité. D’ailleurs Tim Berners-Lee, inventeur du Web, voulait dès sa création “mettre le Web et ses services à la disposition de tous les individus, quel que soit leur matériel ou logiciel, leur infrastructure réseau, leur langue maternelle, leur culture, leur localisation géographique, ou leurs aptitudes physiques ou mentales”. Cet objectif s’étend à nos yeux bien au delà du web et englobe toute l’information numérique. Malheureusement la grande vitesse de développement des TIC laisse peu de place à la réflexion sur leur accessibilité, et les acteurs impliqués se focalisent sur les interfaces-utilisateur dominantes, augmentant ainsi la fracture numérique. Notre activité se situe dans l’étude des modèles informatiques permettant de tirer parti de ces technologies pour améliorer l’accès de tous à la société numérique, et dans l’intégration des principes de ces modèles spécifiques dans les modèles utilisés pour les applications grand public, ce qui peut être une façon de définir le terme “accessibilité numérique”. Nous aborderons différents aspects de l'accessibilité aux documents numériques et en particulier les problèmes posés par les documents scientifiques, contenant des expressions mathématiques.


Web sémantique : données liées et sémantique des schémas Fabien Gandon, INRIA Sophia Antipolis

Web sémantique, web de données, web 3.0, etc. de plus en plus d’acteurs participent à l’extension du web tel que nous le connaissons avec des données et des schémas de données permettant de nouvelles fonctionnalités et un niveau encore inégalé d’interopérabilité des services du web. Le web sémantique propose un jeu de langages permettant de publier et consommer des données liées et la sémantique des schémas de ces données : RDF, RDFS, OWL, SPARQL, etc. De plus en plus d’organisations privées et publiques participent à ce web de données en publiant dans ces langages des données ouvertes et leurs modèles de données non seulement sur le web ouvert mais aussi sur leurs intranets permettant de nouvelles applications internes transversales aux systèmes d’informations existants. Nous revisiterons ensemble les formalismes qui permettent cette évolution, les principes de base derrière chacun d’eux, leurs caractéristiques et ce que chacun apporte à cette nouvelle architecture du Web. Nous essaierons aussi d’illustrer à chaque étape ce que ces standards permettent en termes de nouvelles interactions et fonctionnalités, et les verrous scientifiques qui restent à ouvrir. Enfin nous présenterons quelques travaux de recherche de l’équipe Edelweiss de l’INRIA notamment sur l’intégration et l’exploitation de ces langages dans les applications et usages du web social ou web 2.0.


Etat de l'art de la virtualisation du poste de travail", suivie d'une petite démo. Naly Raliravaka, Département d'informatique de l'université d'Orléans

Démonstration Technique


Computing under Vagueness Apostolos SYROPOULOS, Greek Molecular Computing Group

After introducing the notion vagueness, I will talk about the various expressions of vagueness with emphasis on fuzzy set theory. In particular, I will introduce the basic set operations and I will briefly discuss the relationship of fuzzy set theory to probability theory. Next, I will discuss Zadeh's early ideas on fuzzy algorithms and fuzzy Turing machines. Then, I will formally introduce fuzzy Turing machines and fuzzy P systems. Also, I will talk about the notion of process similarity, fuzzy labeled transition systems, and finally the fuzzy chemical abstract machine.


Analyse statique du noyau de XEN avec l'outil Frama-C. Retour d'expérience. Nikolai Kosmatov , CEA Saclay

We describe our experience of static analysis of the XEN 3.0.3 hypervisor using the Frama-C static analysis tool. The analysis of six selected functions (five hypercalls and the main initialization function) has produced 170 alarms. We have classified these warnings into several categories and examined each of them precisely, using the source code, its preprocessed version and the publicly available documentation. We could conclude on 36 cases among 170, the others were left as unknown errors. Their investigation needs further knowledge of the XEN code and higher precision of the analysis.


Deciphering complex molecular systems: a new ambition for computer science and visualization Matthieu Chavent, CEA - DIF Arpajon

During this talk, we will take a look of recent contributions from computer science field that can drastically improve and enhance molecular visualization. We will see that the majority of these new developments take clearly advantage of new GPUs capabilities. Then, we will present a new molecular representation that we have designed using GPU capabilities. This new representation, called HyperBalls, is really useful to display a broad range of molecules from small atomic structures to huge macromolecular assemblies with high-quality of rendering and lighting.


Bioniformatics, finding protein patterns in genoms FOROUGHMAND ARAABI Mohammad Hadi, University of Tehran

Protein patterns are combinatorial structures describing protein families. Since proteins are biologically translated from genome, protein families can be described also by genome patterns. Dealing with genome patterns introduces a new bio-informatics problem: searching genomic patterns in genome. In this seminar, we will present an overview of biological process of translating proteins from genome, structure and importance of protein and genomic patterns, and algorithms for searching genomic patterns in genome.


L'inférence grammaticale : du coeur de la discipline aux applications Jean-Christophe Janodet, Machine Learning Research Team - Laboratoire Hubert Curien-St Etienne

L'inférence grammaticale est une branche de l'apprentissage automatique où l'on cherche à identifier, de façon exacte ou approximative, des modèles de données structurées, typiquement des automates ou des grammaires de mots, d'arbres ou de graphes. C'est un domaine de recherche qui entretient des relations nombreuses et fécondes avec des domaines comme le model checking, l'apprentissage statistique, le TAL, la bioinformatique ou la reconnaissance des formes. Ainsi, après une introduction au domaine où nous montrerons quelques-uns de nos résultats, nous nous concentrerons sur un problème plus spécifique, liés à la classification d'images, où nous esquisserons les pistes que nous cherchons à suivre actuellement. Nous tâcherons, dans ce cadre, de suggérer des collaborations qui nous semblent possibles avec les membres du LIFO.


Construction des automates Büchi pour le model checking LTL, verifié en Isabelle/HOL Jan Smaus , Research Group Foundations of Artificial Intelligence - Freiburg

On présente l'implantation d'une traduction Isabelle/HOL des formules LTL en automates Büchi. Dans le model checking basé sur les automates, les systèmes sont modelisés comme des systèmes de transitions, et les proprietés de correction donnés comme formules en logique temporelle sont traduites dans des automates correspondants. Une formule LTL est representé comme un automate de Büchi qui accepte précisament les comportements permis par la formule. Le problème de model checking est ainsi reduit au problème d'inclusion entre deux automates. La construction de l'automate est donc une partie essentielle d'un algorithme pour le model checking en LTL. Nous avons implanté une traduction standard de Gerth et al. La correction et la terminaison de notre implantation sont prouvées en Isabelle/HOL, et du code éxecutable est géneré par le génerateur de code d'Isabelle/HOL. Ce travail fait partie d'un effort plus géneral à verifier des algorithmes de model checking en Isabelle/HOL. J'ai acquéris un projet de recherche dans cette thématique et je vais dire quelques mots generaux sur cette thématique.


Sur l'énumération des arbres enrichis Daniele Gardy , Prism Versailles

Prenons une expression logique du calcul des propositions: elle peut être représentée sous forme arborescente. Suivant les règles de construction de la formule, l'arbre sera binaire ou non, planaire ou non, et étiqueté avec différents connecteurs ou littéraux. L'énumération de tels arbres, et l'étude de leurs propriétés statistiques, sont un domaine classique d'application de la combinatoire analytique. Prenons maintenant une formule du calcul des prédicats: l'existence de quantificateurs fait que nous ne pouvons plus a priori utiliser une représentation arborescente. Il est cependant possible de voir une telle formule sous la forme d'un arbre, auquel on aurait ajouté des arcs partant de certains noeuds (ceux correspondant aux quantificateurs) et allant vers des feuilles. De manière équivalente, cela revient à colorer ces arbres selon certaines règles. L'énumération de telles structures, que nous appelons des arbres enrichis, ne peut plus se faire suivant les techniques classiques d'énumération d'arbres, et requiert de nouvelles approches. Nous présenterons en particulier deux classes restreintes d'arbres enrichis, pour lesquelles des résultats d'énumération ont été obtenus.


Unconventional Architectures: The Art of Programming Self-Organization René Doursat , Ecole polytechnique - CNRS

On the one hand, natural phenomena of spontaneous pattern formation are generally random and repetitive, whereas, on the other hand, complicated heterogeneous architectures are generally the product of human design. Between these two poles, multicellular organisms and social insect constructions are rather unique examples of natural systems that exhibit both self-organization and a strong architecture. Can we export their precise self-formation capabilities to technological systems? To address this challenge, I have proposed a new research field called “Morphogenetic Engineering”, which explores the artificial design and implementation of autonomous systems capable of developing complex, heterogeneous morphologies without central planning or external drive. Particular emphasis is set on the programmability and controllability of self-organization, properties that are often underappreciated in complex systems science—while, conversely, the benefits of genuine self-organization are often underappreciated in engineering methodologies. I present here two related studies in morphogenetic engineering. First, a multi-agent model of biological development that combines pattern formation (based on gene regulation networks and positional gradients) and self-assembly (arising from mechanical forces between cells). A direct application of this model is the design of robotic swarms able to display various kinds of group behavior depending on the environment—often by self- aggregating into specific formations and superstructures. Second, generalizing from 2-D/3-D multicellular organisms to N-D networks, a model of self- organization of complex but precise graph topologies by “programmed attachment” based on dynamical opening of node ports, spread of gradients and creation of links. This model potentially has implications for “autonomic networks” and “multi-agent systems” broadly, which all rely on a myriad of mobile devices, software agents and/or human users following only local rules and peer-to-peer communication.


Analyse de la complexité des algorithmes d'apprentissage relationnel Aomar Osmani, Laboratoire D'informatique de Paris nord-LIPN

L'apprentissage relationnel (AR) est adapté aux applications où les données sont décrites dans les bases de données, mais il souffre cruellement du problème de passage à l'échelle. En cause les deux sources de complexité qui sont le test de couverture et la recherche dans l'espace d'hypothèses qui font du problème d'AR un problème $\Sigma^2$ difficile. Cette complexité est obtenue dans le cadre d'analyse du pire cas où le modèle théorique de référence en apprentissage est le modèle PAC. La plupart des résultats théoriques sont obtenus dans ce cadre. Les questions qu'il est légitime de se poser sont : quel est l'impact de ces résultats sur des applications réelles ? Quelle est la qualité des meilleurs algorithmes développés pour résoudre ces problèmes sur des applications réelles ? En AR, la réponse est sévère : il n'existe aucun algorithme capable de résoudre le problème de cohérence de l'apprentissage en un temps raisonnable pour des applications ayant quelques dizaines de variables. D'un autre coté, l'analyse de la complexité en moyenne paraît être plus applicable, car elle ne s'intéresse pas au coût de la résolution du problème le plus difficile, mais à l'évaluation de la complexité de la résolution en moyenne des problèmes. Évidemment, il est difficile voire impossible de donner une distribution exacte des problèmes liés aux applications réelles, mais en considérant des distributions simples et des générateurs respectant ces distributions, il est possible de concevoir des solutions plus praticables que celles qui sont proposées par les études s'intéressant aux pires des cas. Les travaux effectués en intelligence artificielle depuis une vingtaine d'années ont montré une corrélation entre l'étude de la complexité en moyenne et la difficulté de la résolution des problèmes. En suivant certains paramètres, il est possible de regrouper les problèmes en fonction de leur complexité. Une transition de phases apparaît systématique dans la zone de concentration des problèmes difficiles. Dans ce modèle, bien étudié pour la résolution des problèmes de recherche, la complexité calculatoire est modélisée comme une variable aléatoire qui dépend de certains paramètres de contrôle de la classe de problème considérée. La complexité est alors modélisée comme une distribution sur les instances des problèmes à traiter. L'objectif de notre travail est de poser les base d'un cadre d'analyse alternatif au modèle d'analyse dans le pire des cas dans le but d'explorer des techniques de recherche mieux adaptées aux applications réelles. Nous nous sommes intéressés à la version cohérence de l'apprentissage relationnel et avons isolé les sources de complexité de ce problème. Nous avons proposé un modèle présentant des bonnes propriétés pour l'évaluation d'algorithmes qui exhibe une transition de phase même pour des problèmes de petite taille. Nous avons évalué les algorithmes représentatifs en apprentissage relationnel dans ce cadre.


Constraint-Based Scheduling for Steel Production Guido Tack, Department of Computer Science - K.U. Leuven

Modern steel plants are highly integrated factories, producing different types of steel, often in a just-in-time fashion (i.e., producing for customer demand, not for stock). The processes in these factories require careful scheduling in order to meet deadlines, maintain a high product quality, and keep the machines busy. Guido Tack is a researcher at K.U.Leuven, Belgium, working in a project with PSI Metals, a Brussels-based company that provides software solutions for the steel industry. In this talk, he will give an overview of the processes involved in steel production, and discuss one particular combinatorial problem, called Real-time Heat Scheduling. The talk will cover two different approaches to solving this problem - one based on mixed integer programming, the other based on constraint programming.


Indécidabilité, pavages et polyominos Nicolas Ollinger, LIF Marseille

Un polyomino est une figure finie simplement connexe obtenue en collant des carrés unité les uns aux autres arête à arête. Une famille de polyominos pave le plan si on peut recouvrir le plan euclidien avec des copies de ces polyominos sans chevauchement et sans trou. Dans cet exposé, on étudie le problème de décision suivant : étant donnée une famille finie de polyominos, pave-t-elle le plan ? Dans un premier temps, on redémontrera l'indécidabilité du problème à l'aide du Domino Problem, introduit par Wang en 1961. Puis, on s'intéressera à la famille de problèmes de décision indexée par la taille de la famille de polyominos et on montrera qu'il existe une frontière entre décidable et indécidable pour ce paramètre. On conclura par quelques problèmes ouverts intrigants et l'existence d'une famille de 5 polyominos qui pave le plan uniquement de manière non récursive.


Logiques modales avec comptage Guillaume Hoffmann, laboratoire LORIA, Université Henri Poincaré, Nancy

Nous présentons un langage modale incluant des opérateurs qui comptent explicitement le nombre d'éléments qu'un modèle inclut dans l'extension d'une formule. Nous montrons comment cette logique a été précédemment étudiée sous divers aspects. Nous explicitons les liens avec la "graded modal logic" et la logique hybride. Nous illustrons une application possible du langage au traitement des requêtes en langage naturel. Nous explorons le pouvoir expressif de cette logique avec des bisimulations, ainsi que la complexité de son problème de satisfiabilité, et définissons une tâche d'inférence qui récupère la cardinalité de l'extension d'une formule donnée, et fournissons un algorithme pour l'effectuer.


Algorithmes de chiffrement/déchiffrement basé chaos pour la sécurité des images transmises. Abir Awad, LIFO

La mondialisation des échanges (Internet, messagerie électronique, commerce électronique, …), grâce à l’émergence des nouvelles technologies de l’information et de la communication, pose le problème de la sécurité de l’information transmise à travers les canaux publics non sécurisés. L’utilisation du chaos dans des crypto-systèmes, apporte de l’amélioration par rapport aux méthodes standards de la cryptographie (DES, IDEA, AES), ceci grâce aux caractéristiques des signaux chaotiques tels que : bonnes propriétés cryptographiques, reproductibilité à l’identique (déterministes), et l’hyper sensibilité à la clé secrète. Dans cette présentation, des nouvelles méthodes de cryptographie basé chaos sont présentées. La carte chaotique utilisée inclut une technique de perturbation permettant d’améliorer les dynamiques chaotiques et ainsi d’augmenter et de contrôler la longueur des séquences chaotiques générées. L’analyse de la sécurité des algorithmes de chiffrement proposées, utilisant les tests standards les plus significatifs : sensibilité (à la clé secrète en émission et en réception, et à l’image claire), tests statistiques (histogramme, densité de probabilité, corrélation des pixels adjacents…) sur l’image claire et l’image chiffrée, série des tests statistiques de NIST sur des images chiffrées montre l’intérêt des structures proposées.


Toponym Disambiguation in Geographical Information Retrieval Davide Buscaldi, LIFO

Text-based Information Retrieval systems must deal with the problem of lexical ambiguity. In my Ph.D. thesis I studied a specific kind of ambiguity related to place names, or toponyms, and how this kind of ambiguity affects the accuracy in retrieving geographically-constrained information. In this talk I will resume the most important findings of my Ph.D. thesis, highlighting the problems related to the granularity of the task, the choice of a particular resource and the locality of the target text collection.


Update XML Views Jixue Liu, School of Computer and Information Science, University of South Australia

View update is the problem of translating an update to a view to some updates to the base data of the view. In this paper, we conduct a systematic study of the view update problem in XML databases. We analyze independent factors affecting the translation problem and develop theorems to show the translatability in various cases determined by the factors. We propose translation procedures for the cases where a view update is translatable and prove that the procedures are correct. At the end of the paper, we propose an algorithm and analyze its performance.


ATI Tablette graphique Sophie Robert et Mathieu Liedloff , LIFO

à venir


Réunion de département, Dpt Informatique - UFR Sciences