• Accueil du LIFO
• Personnes (Annuaire)
• Équipes
• CA
• GAMoC
• LMV
• Pamda
• SDS
• Actions de Recherche
• Thèses en cours
• Séminaires et Evénements
• Séminaires
• Evénements au LIFO
• Evénements hors LIFO
• Publications et logiciels
• Publications
• Thèses et Habilitations
• Rapports de Recherche
• Logiciels
• Transfert de technologie

• Renseignements pratiques
• Organisation
• Accès
• Enseignement
• Pôle Informatique
• IUT Informatique
• 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

Les séminaires du LIFO

28/06/2019 : soutenance de thèse : Analyse statique des programmes BSPlib
Arvid Jakobsson (LIFO) Résumé
Attention : Débute à 10 h. Lieu : salle Soutenance de Thèse (Salle 101), 1er Étage au Bâtiment S (Faculté Des Sciences)

28/06/2019 : Soutenance de thèse : génération automatique de code parallèle isochrone
Thibaut Tachon (LIFO) Résumé
Attention : Débute à 14 h 30. Lieu : salle Soutenance de Thèse (Salle 101), 1er Étage au Bâtiment S (Faculté Des Sciences)

24/06/2019 : Real Time Data Mining
João Gama (University of Porto/LIAAD/INESC) Résumé
Attention : Débute à 13 h 45.

14/06/2019 : Soutenance de thèse : Construction semi-automatique d’une grammaire d’arbres adjoints pour l’analyse syntaxico-sémantique de l’arabe
Chérifa Ben Khelil (LIFO) Résumé
Attention : Débute à 09 h. Lieu : Amphi H, bâtiment 3IA

03/06/2019 : Homomorphismes navigationnels pour les requêtes dans les bases de données graphes
Florent Foucaud (LIFO) Résumé
Attention : Débute à 15 h.

20/05/2019 : sémantique distributionnelle appliquée à un corpus diachronique
Guillaume Desagulier et Ilaine Wang (MoDyCo (Paris 8) et LIFO) Résumé
Attention : Débute à 13 h 45.

06/05/2019 : Caractérisation logique du temps minimal des automates cellulaires
Théo Grente (GREYC, Université de Caen Normandie) Résumé
Attention : Débute à 13 h 45.

29/04/2019 : On the Parameterized Complexity of Graph Modification to First-Order Logic Properties
Petr Golovach (Université de Bergen, Norvège) Résumé
Attention : Débute à 13 h 45.

18/03/2019 : Bisplit graphs satisfy the Chen-Chvátal conjecture
Matthieu Rosenfeld () Résumé
Attention : Débute à 13 h 45.

11/02/2019 : An overview of the Tezos blockchain
Mathias Bourgoin (Nomadic Labs) Résumé
Attention : Débute à 13 h 45.

Résumés des séminaires

soutenance de thèse : Analyse statique des programmes BSPlib Arvid Jakobsson, LIFO
Membres du jury : KUCHEN, Herbert – Professeur, WWU Münster BARTHOU, Denis – Professeur, Université de Bordeaux BOUSDIRA-SEMMAR, Wadoud – Maître de conférence, Université d’Orléans DABROWSKI, Frédéric – Maître de conférence, Université d’Orléans HAINS, Gaétan – Chercheur-Ingénieur, Huawei Technologies SUIJLEN, Wijnand – Chercheur-Ingénieur, Huawei Technologies LOULERGUE, Frédéric – Professeur, Northern Arizona University et Université d’Orléans CHAILLOUX, Emmanuel – Professeur, Sorbonne Université Résumé de la thèse : La programmation parallèle consiste à utiliser des architectures à multiples unités de traitement, de manière à ce que le temps de calcul soit inversement proportionnel au nombre d'unités matérielles. Le modèle de BSP (Bulk Synchronous Parallel) permet de rendre le temps de calcul prévisible. BSPlib est une bibliothèque pour la programmation BSP en langage C. En BSPlib on entrelace des instructions de contrôle de la structure parallèle globale, et des instructions locales pour chaque unité de traitement. Cela permet des optimisations fines de la synchronisation, mais permet aussi l'écriture de programmes dont les calculs locaux divergent et masquent ainsi l'évolution globale du calcul BSP. Toutefois, les programmes BSPlib réalistes sont syntaxiquement alignés, une propriété qui garantit la convergence du flot de contrôle parallèle. Dans ce mémoire nous étudions les trois dimensions principales des programmes BSPlib du point de vue de l'alignement syntaxique: la synchronisation, le temps de calcul et la communication. D'abord nous présentons une analyse statique qui identifie les instructions syntaxiquement alignées et les utilise pour vérifier la sûreté de la synchronisation globale. Cette analyse a été implémentée en Frama-C et certifiée en Coq. Ensuite nous utilisons l'alignement syntaxique comme base d'une analyse statique du temps de calcul. Elle est fondée sur une analyse classique du coût pour les programmes séquentiels. Enfin nous définissons une condition suffisante pour la sûreté de l'enregistrement des variables. L'enregistrement en BSPlib permet la communication par accès aléatoire à la mémoire distante (DRMA) mais est sujet à des erreurs de programmation. Notre développement technique est la base d'une future analyse statique de ce mécanisme. Mots clés : Programmation parallèle, Bulk Synchronous Parallelism, SPMD, Analyse statique, Synchronisation, Analyse de coût, Communication

Soutenance de thèse : génération automatique de code parallèle isochrone Thibaut Tachon, LIFO
Membres du jury : M. Frederic LOULERGUE Université d'Orléans et Northern Arizona University Directeur de thèse M. Franck POMMEREAU Université d'Evry Rapporteur M. John MULLINS École Polytechnique de Montréal Rapporteur M. Gaétan HAINS Huawei Technologies France S.A.S.U. Examinateur M. Wijnand SUIJLEN Huawei Technologies France S.A.S.U. Examinateur M. Jean-michel COUVREUR Université d'Orléans - Faculté des sciences Examinateur Résumé : Depuis la stagnation de la fréquence d’horloge des processeurs, l’accroissement de la puissance de calcul a dépendu entièrement de l’accroissement du nombre d’unités de calcul. Plus que la difficulté algorithmique impliquée par l’écriture de tout programme séquentiel, la programmation parallèle demande au programmeur de gérer de nombreuses unités de calcul, incluant leurs tâches et leurs interactions. Pour alléger le fardeau du programmeur, cette thèse propose deux approches différentes de génération automatique de code parallèle. Le modèle parallèle isochrone BSP possède des propriétés intéressantes telles que son modèle de coût qui en font la cible de notre génération de code parallèle. Les automates et expressions régulières sont souvent choisis pour modéliser les calculs séquentiels et leurs parallélisation devrait, à long terme, aboutir à de solide fondations pour la génération de code parallèle. Pour notre approche principale, nous développons la théorie des automates BSP avec leur génération et déterminisation. Cette théorie est utilisé dans une nouvelle méthode pour la recherche de motif à l’aide d’expressions régulières. Notre autre approche propose un langage spécifique au domaine des réseaux de neurones où la composition fonctionnelle d’un petit nombre de primitives facilite le développement, la maintenance et la définition formelle du langage par rapport aux approches existantes.

Real Time Data Mining João Gama, University of Porto/LIAAD/INESC
Nowadays, there are applications in which the data are modelled best not as persistent tables, but rather as transient data streams. In this keynote, we discuss the limitations of current machine learning and data mining algorithms. We discuss the fundamental issues in learning in dynamic environments like learning decision models that evolve over time, learning and forgetting, concept drift and change detection. Data streams are characterized by huge amounts of data that introduce new constraints in the design of learning algorithms: limited computational resources in terms of memory, processing time and CPU power. In this talk, we present some illustrative algorithms designed to taking these constrains into account. We identify the main issues and current challenges that emerge in learning from data streams, and present open research lines for further developments.

Soutenance de thèse : Construction semi-automatique d’une grammaire d’arbres adjoints pour l’analyse syntaxico-sémantique de l’arabe Chérifa Ben Khelil, LIFO
MEMBRES DU JURY : - Chiraz BEN OTHMANE ZRIBI, Maître de Conférences, ENSI La Manouba - Denys DUCHIER, Professeur, Université d’Orléans - Claire GARDENT, Directrice de Recherche, CNRS-LORIA UMR 7503 - Kais HADDAR, Professeur, Université de Sfax - Laura KALLMEYER, Professeur, Université de Düsseldorf - Yannick PARMENTIER, Maître de Conférences, Université de Lorraine RÉSUMÉ Cette thèse traite de la description formelle et du développement d’une grammaire électronique de la langue arabe. Ce travail est un prérequis à la création d’outils de traitement automatique de l’arabe. Cette langue présente de nombreux challenges pour un traitement automatique, en effet l’ordre de mots en arabe est relativement libre, la morphologie y est riche et les diacritiques sont omis dans les textes écrits. Bien que plusieurs travaux de recherche aient abordé certaines de ces problématiques, les ressources électroniques utiles pour le traitement de l’arabe demeurent relativement rares ou encore peu disponibles. Dans ce travail de thèse, nous nous sommes intéressés à la représentation de la syntaxe (ordre des mots) et du sens de l’arabe standard moderne. Comme système formel de représentation de la langue, nous avons choisi le formalisme des grammaires d’arbres adjoints (Tree Adjoining Grammar). Nous avons ainsi proposé une grammaire d’arbres adjoints électronique de l’arabe nommée « ArabTAGv2 ». Cette ressource réutilise en partie la modélisation pré-existante dans la grammaire définie manuellement «ArabTAG » et l’intègre à une représentation abstraite appelée métagrammaire. L’expert linguiste peut ainsi décrire la syntaxe et sémantique de la langue avec des outils d’abstraction facilitant la maintenance et l’extension de la grammaire. La grammaire ainsi décrite compte 1074 règles syntaxiques (non lexicalisées) et 27 cadres sémantiques (relations prédicatives). Cette ressource a été évaluée en analysant un corpus issu d’extraits d’un manuel scolaire d’apprentissage de l’arabe.

Homomorphismes navigationnels pour les requêtes dans les bases de données graphes Florent Foucaud, LIFO
Certaines requêtes de bases de données peuvent être modélisées par des homomorphismes de structures relationnelles. Les bases de données graphes sont de plus en plus utilisées dans l'industrie. Une telle base de données peut être modélisée par un (grand) graphe orienté et étiqueté. Certaines requêtes "locales" peuvent être vues comme de (petits) graphes orientés et étiquetés, et la requête est satisfaite s'il existe un homomorphisme du graphe de la requête vers le graphe de la base de données. Dans les applications modernes, des requêtes plus expressives, dites "navigationnelles", sont communément utilisées. Nous montrerons comment définir la notion correspondante d'homomorphisme navigationnel, concept défini récemment par Barcelo, Romero et Vardi. Nous nous focaliserons sur les requêtes dites "à chemins réguliers", définies par des langages réguliers, et nous présenterons quelques résultats algorithmiques théoriques dans ce domaine. Nous montrerons le lien entre cette thématique et celles de la théorie des homomorphismes de graphes et des problèmes de satisfaction de contraintes. Il s'agit de travaux réalisés avec Laurent Beaudou, Florent Madelaine, Lhouari Nourine et Gaétan Richard.

sémantique distributionnelle appliquée à un corpus diachronique Guillaume Desagulier et Ilaine Wang, MoDyCo (Paris 8) et LIFO
Nous abordons la question de l'évolution du sens en corpus sous l'angle de la sémantique distributionnelle. Il s'agit pour nous de déduire l'évolution sémantique de marqueurs linguistiques par l'examen de préférences collocationnelles à travers les époques. Deux questions se posent : comment distinguer les principales étapes de l'évolution sémantique d'un marqueur ? Quelle granularité adopter : la distinction artificielle en années ou en décennies proposée par défaut dans les corpus ou une distinction plus naturelle dérivée de la distribution des données ? Nous passons en revue trois méthodes distributionnelles : deux relevant de la linguistique de corpus et une relevant du traitement automatique des langues. La première méthode, VNC (Variability-based Neighbour Clustering), est fondée sur la classification ascendante hiérarchique. Elle procède à une périodisation automatique. Le regroupement de périodes en fonction de leurs similitudes se fait sur la base du principe d'adjacence temporelle. La seconde méthode est une illustration classique des modèles de sémantique distributionnelle. La forme cible est extraite d'un corpus au sein d'une fenêtre contextuelle. Une matrice de co-occurrences est calculée puis transformée à l'aide d'une mesure appelée PPMI (Positive Pointwise Mutual Information). Les dimensions de la matrice ainsi pondérée est réduite par SVD (Singular Value Decomposition) et projetée sur un espace à deux dimensions à l'aide de t-SNE. L'évolution sémantique est capturée par des contours dont le centre de gravité change en fonction des époques. La troisième méthode, HistWords (https://nlp.stanford.edu/projects/histwords/), est proche de la seconde. Elle est inspirée de word2vec. Il s'agit d'un algorithme permettant de tracer l'évolution sémantique de lexèmes sur la base de vecteurs calculés avec la méthode Skip-Gram with Negative Sampling (SGNS). Deux études de cas sont abordées : le split infinitive en anglais (to boldly go where no man has gone before) et les intensifieurs de l'anglais (quite, rather, fairly, pretty, tremendously, utterly, jolly, etc.).

Caractérisation logique du temps minimal des automates cellulaires Théo Grente, GREYC, Université de Caen Normandie
Les automates cellulaires représentent le modèle par excellence du calcul parallèle et local. De la même façon qu’on sait caractériser en logique les langages rationnels, on cherche à caractériser/programmer en logique les calculs des automates cellulaires. Le comportement local et déterministe des automates cellulaires s'exprime naturellement par des clauses de Horn portant sur une arithmétique locale du prédécesseur. L'outil principal utilisé est une méthode de normalisation transformant une formule en une formule équivalente qui imite un circuit grille. Dans cet exposé, je présenterai l'exemple du temps réel (= temps minimal) des automates cellulaires, intéressant par sa puissance de reconnaissance (multiplication d'entiers, majorité...) et son polymorphisme.

On the Parameterized Complexity of Graph Modification to First-Order Logic Properties Petr Golovach, Université de Bergen, Norvège
We establish connections between parameterized/kernelization complexity of graph modification problems and expressibility in logic. For a first-order logic formula \phi, we consider the problem of deciding whether an input graph can be modified by removing/adding at most k vertices/edges such that the resulting modification has the property expressible by \phi. We provide sufficient and necessary conditions on the structure of the prefix of \phi specifying when the corresponding graph modification problem is fixed-parameter tractable (parameterized by k) and when it admits a polynomial kernel.

Bisplit graphs satisfy the Chen-Chvátal conjecture Matthieu Rosenfeld,
Un des théorèmes de De Bruijn-Erdos énnonce qu’étant donné un ensemble S de n points du plan soit ils sont colinéaires, soit ils génèrent au moins n droites. On commencera par une démonstration élémentaire de ce résultat. L’un des candidats naturels pour étendre ce résultat est l’ensemble des lignes définies par un système de betweenness (“entritude”). On peut associer à tout système métrique un tel système de betweenness et se demander si le théorème de De Bruijn-Erdos s’applique encore. La question est toujours ouverte et ce en particulier dans les graphes. Nous donnerons toutes les définitions nécessaires et discuterons du cas des graphes plus en détail et en particulier des graphes bisplit.

An overview of the Tezos blockchain Mathias Bourgoin, Nomadic Labs
Blockchains, such as Bitcoin or Ethereum, are distributed and decentralized ledgers. Bitcoin was, in 2009, the first blockchain, allowing financial transactions using a cryptocurrency. Then new blockchains such as Ethereum introduced smart contracts, small computer programs running in the blockchain and Dapps, distributed applications running on the blockchain (through smart contracts). These blockchains are based on an energy consuming 'proof of work' consensus algorithm and their governance is informal and can lead to hard forks of the blockchain. In this talk, I will present Tezos, an innovative self-amending blockchain that - provides a formal *on-chain governance* mechanism to activate upgrades without the need for hard forks. - focuses on *security* (through formal verification) and provides an environment to run formally verifiable smart contracts. - also replaces the classic 'proof of work' consensus algorithm with a modern, resilient and energy efficient (thus ecological) *'proof of stake'* algorithm.