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


17/12/2014 : Gamma-pomset pour la modélisation et la vérification de systèmes parallèles (Soutenance de thèse)
Mouhamadou Sakho (LIFO, Université d'Orléans) Résumé
Attention : Cette soutenance a lieu un mercredi. Lieu : Amphi Herbrand, bâtiment 3IA

15/12/2014 : Requetes Datalog sur des structures de graphes: le cas de la logique monadique du second ordre et le cas des modeles de requetes.
Eugenie Foustoucos (Computer Science Department of the Athens University of Business and Economics) Résumé
Attention : Débute à 13 h 30.

15/12/2014 : Sections atomiques emboîtées avec échappement de processus légers : sémantiques et compilation (Soutenance de thèse)
Thomas Pinsard (LIFO, Université d'Orléans) Résumé
Attention : Débute à 14 h 30. Lieu : Bâtiment S

12/12/2014 : Coloriage du plan discret par jeux de tuiles déterministes (Soutenance de thèse)
Bastien Le Gloannec (LIFO, Université d'Orléans) Résumé
Attention : Cette soutenance aura lieu un vendredi. Lieu : Amphi H, bâtiment 3IA

11/12/2014 : Développement Modulaire de Grammaires Formelles (Soutenance de thèse)
Simon Petitjean (LIFO, Université d'Orléans) Résumé
Attention : Cette soutenance aura lieu un jeudi / Débute à 13 h 30. Lieu : Amphi H, bâtiment 3IA

10/12/2014 : Constrained Clustering by Constraint Programming (Soutenance de thèse)
Chuong Duong Khanh (LIFO, Université d'Orléans) Résumé
Attention : Cette soutenance aura lieu un mercredi / Débute à 13 h 30. Lieu : Amphi Herbrand, bâtiment 3IA

08/12/2014 : Prédiction de la qualité en traduction automatique : problèmes d'évaluation et limitations des systèmes supervisés
Erwan Moreau (Trinity College Dublin, Ireland) Résumé

01/12/2014 : SQL/AA : Privacy-Preserving Query Execution using a Decentralized Architecture and Tamper Resistant Hardware
Benjamin Nguyen (LIFO, INSA Centre Val de Loire) Résumé

28/11/2014 : Comparaison et évolution de schémas XML (Soutenance de thèse)
Joshua Amavi (LIFO, Université d'Orléans / LI, Université de Tours) Résumé
Attention : cette soutenance aura lieu un vendredi / Débute à 10 h. Lieu : Amphi H, bâtiment 3IA

17/11/2014 : Proposition de combinaison de systèmes en TAL : annotations partielles et décomposition duale
Joseph Le Roux (Laboratoire d'Informatique de Paris Nord, Université Paris 13) Résumé

03/11/2014 : Décompositions de trigraphes
Antoine Mamcarz (LIFO, Université d'Orléans) Résumé

13/10/2014 : Introduction à la vérification déductive avec Frama-C
Virgile Prevosto (CEA LIST) Résumé

29/09/2014 : Modélisation et implémentation de parallélisme implicite pour les simulations scientifiques basées sur des maillages (Soutenance de thèse)
Hélène Coullon (LIFO, Université d'Orléans) Résumé

04/07/2014 : Challenging machine learning classification tasks
André Carlos Ponce Leon Ferreira de Carvalho (Universidade de São Paulo at São Carlos, Brazil) Résumé
Attention : Ce séminaire aura exceptionnellement lieu un vendredi.

23/06/2014 : A Graph Reduction Machine for Web Service Compositions
Martin A. Musicante (Federal University of Rio Grande do Norte, Department of Computer Science, Natal, Brazil) Résumé

16/06/2014 : Vers la construction à large couverture de la représentation du sens de phrases de langue naturelle
Benoît Crabbé (Université Paris Diderot-Paris 7, INRIA Rocquencourt) Résumé

12/05/2014 : On the Context-Freeness Problem for Vector Addition Systems
Grégoire Sutre (Laboratoire LaBRI - CNRS - Université de Bordeaux ) Résumé

05/05/2014 : Les capitalistes sociaux : les sentiers de la gloire sur Twitter
Nicolas Dugué (LIFO - Université d'Orléans) Résumé

28/04/2014 : A Linear-Time Algorithm for Computing the Prime Decomposition of a Directed Graph With Regard to the Cartesian Product
Christophe Crespelle (LIP - ENS Lyon) Résumé

14/04/2014 : Design de structures d'ARN avec contraintes de séquence : une approche à base de langages formels
Alain Denise (Université Paris Sud) Résumé

14/04/2014 : Vers l'analyse statique de langages fonctionnels par réécriture et automates d'arbres
Thomas Genet (IRISA, Université de Rennes) Résumé
Attention : 2e séminaire de l'après-midi / Débute à 15 h.

07/04/2014 : Mesure de performance des algorithmes de routage pour le HPC
Matthieu Perotin (BULL Extreme Computing R&D, Bruyères-Le-Châtel) Résumé

17/03/2014 : Systèmes multi-agents et culture
Loïs Vanhée (Université Montpellier 2 et Universiteit Utrecht) Résumé

10/03/2014 : Systèmes complexes : des réseaux génétiques à la ségrégation urbaine
Eric Goles (Adolfo Ibáñez University, Santiago, Chili) Résumé
Attention : Le séminaire aura lieu dans la salle de séminaire du bâtiment de mathématiques (MAPMO).

03/03/2014 : Several aspects of probabilistic cellular automata
Damien Regnault (IBISC - Université Evry-Val d'Essonne) Résumé

17/02/2014 : Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components
Arnaud Lanoix (LINA, Université de Nantes) Résumé
Attention : Le titre, l’abstract et les slides seront en anglais, mais l’exposé sera en français.

10/02/2014 : Une vue d'ensemble de l'extraction Coq
Pierre Letouzey (PPS - Université Paris Diderot-Paris 7) Résumé

27/01/2014 : First impressions about the use of an embedded low-power manycore processor for HPC
Marcio Castro (Universidade Federal do Rio Grande do Sul (Brazil)) Résumé

20/01/2014 : Extraction de code fonctionnel à partir de spécifications inductives
Catherine Dubois (ENSIIE) Résumé


Résumés des séminaires


Gamma-pomset pour la modélisation et la vérification de systèmes parallèles (Soutenance de thèse) Mouhamadou Sakho, LIFO, Université d'Orléans

Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle Gamma-Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les Gamma-Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les Gamma-pomsets.


Requetes Datalog sur des structures de graphes: le cas de la logique monadique du second ordre et le cas des modeles de requetes. Eugenie Foustoucos, Computer Science Department of the Athens University of Business and Economics

Nous présentons deux classes de requêtes et pour chacune d’elles nous démontrons qu’elle est traduisible en Datalog, le langage de requêtes pour bases de données déductives. La première partie de l'exposé traite du formalisme logique très expressif qu'est la logique monadique du second-ordre (MSO) considérée sur les structures d'arbres d'une part et sur les structures de largeur d'arborescence bornée d'autre part: nous montrons que dans les deux cas les requêtes MSO sont exprimables par des requêtes datalog et nous en donnons une traduction effective. Les résultats existant sur la connexion MSO-datalog concernent une classe restreinte de requêtes MSO, celle des requêtes dites "MSO unaires".Nos résultats concernent la totalité des requêtes MSO et traitent également de problèmes MSO de comptage. La deuxième partie de l'exposé traite de la conception de requêtes-modèles, le but de celles-ci étant de faciliter l'utilisateur non-expert à questionner un système d'information dont il ignore l'organisation logique. Nous analysons un nombre de catalogues de musées pour aboutir à un ensemble (de taille très raisonnable) de requêtes-modèles relatives au domaine culturel. Ces requêtes sont le modèle de questions récurrentes, jugées importantes. Nous exprimons ces modèles de requêtes par des règles datalog ainsi que par des requêtes SPARQL. Notre approche peut être envisagée pour d'autres domaines (tel le domaine médical) où il serait également souhaitable de fournir une assistance à l'utilisateur au niveau requêtes.


Sections atomiques emboîtées avec échappement de processus légers : sémantiques et compilation (Soutenance de thèse) Thomas Pinsard, LIFO, Université d'Orléans

La mémoire transactionnelle est un mécanisme de plus en plus populaire pour la programmation parallèle et concurrente. Dans la plupart des implantations, l'emboîtement de transactions n'est pas possible ce qui pénalise la modularité. Plutôt que les transactions, qui sont un choix possible d'implantation, nous considérons directement la notion de section atomique. Dans un objectif d'améliorer la modularité et l'expressivité, nous considérons un langage impératif simple étendu avec des instructions de parallélisme avec lancement et attente de processus légers et une instruction de section atomique à portée syntaxique, depuis laquelle des processus légers peuvent s'échapper. Dans ce contexte notre première contribution est la définition précise de l'atomicité et de la bonne synchronisation. Nous prouvons que pour des traces bien formées, la dernière impliquent la forme forte de la première. Ceci est fait sur des traces d'exécution abstraites dans le sens où nous ne définissons par précisément la syntaxe et la sémantique opérationnelle d'un langage de programmation. Cette première partie de notre travail peut être considérée comme une spécification pour un tel langage. Nous avons utilisé l'assistant de preuve Coq pour modéliser et prouver nos résultats. Notre deuxième contribution est la définition formelle du langage Atomic Fork Join (AFJ). Nous montrons que les traces de sa sémantique opérationnelle vérifie effectivement les conditions de bonne formation définies précédemment. La troisième contribution est la compilation de programmes AFJ en programmes Lock Unlock Fork Join (LUFJ) un langage avec processus léger et verrous mais sans sections atomiques. Nous étudions la correction de la compilation de AFJ vers LUFJ.


Coloriage du plan discret par jeux de tuiles déterministes (Soutenance de thèse) Bastien Le Gloannec, LIFO, Université d'Orléans

Nous étudions les propriétés des ensembles de pavages engendrés par des jeux de tuiles de Wang exhibant une ou plusieurs directions de déterminisme local, en accordant une importance toute particulière aux jeux déterministes dans les quatre directions diagonales simultanément, dits 4-way déterministes. Après avoir proposé une construction alternative d'un jeu de tuiles apériodique 4-way déterministe, nous étudions plusieurs problèmes de décision sur ces objets et complétons en particulier le résultat d'indécidabilité du problème du pavage dans le cadre 4-way déterministe établi par Lukkarila en montrant l'indécidabilité du problème du pavage périodique 4-way déterministe. Nous montrons également que des familles complexes de coloriages du plan telles que celles engendrées par les substitutions restent sofiques dans un cadre 4-way déterministe. Nous proposons une bi-déterminisation des constructions de jeux de tuiles point-fixe de Durand, Romashchenko et Shen et en tirons quelques premières applications. Enfin, nous considérons l'opportunité d'élargir le rayon de la règle locale de déterminisme afin de limiter les directions d'expansivité et ainsi de permettre la construction localement déterministe de systèmes de particules et collisions non triviaux. Nous introduisons un nouveau modèle syntaxique commode afin de travailler à rayon deux et revisitons des problématiques de Lukkarila dans ce cadre.


Développement Modulaire de Grammaires Formelles (Soutenance de thèse) Simon Petitjean, LIFO, Université d'Orléans

Les travaux présentés dans cette thèse visent à faciliter le développement de ressources pour le traitement automatique des langues. Les ressources de ce type prennent des formes très diverses, en raison de l'existence de différents niveaux d'étude de la langue (syntaxe, morphologie, sémantique, ...) et de différents formalismes proposés pour la description des langues à chacun de ces niveaux. Les formalismes faisant intervenir différents types de structures, un unique langague de description n'est pas suffisant : il est nécessaire pour chaque formalisme de créer un langage dédié (ou DSL), et d'implémenter un nouvel outil utilisant ce langage, ce qui est une tâche longue et complexe. Pour cette raison, nous proposons dans cette thèse une méthode pour assembler modulairement, et adapter, des cadres de développement spécifiques à des tâches de génération de ressources langagières. Les cadres de développement créés sont construits autour des concepts fondamentaux de l'approche XMG (eXtensible MetaGrammar) à savoir : disposer d'un langage de description permettant la définition modulaire d'abstractions sur des structures linguisitques, ainsi que leur combinaison non-déterministe (i.e. au moyen des opérateurs logiques de conjonction et disjonction). La méthode se base sur l'assemblage d'un langage de description à partir de briques réutilisables, et d'après un fichier unique de spécification. L'intégralité de la chaîne de traitement pour le DSL ainsi défini est assemblée automatiquement d'après cette même spécification. Nous avons dans un premier temps validé cette approche en recréant l'outil XMG à partir de briques élémentaires. Des collaborations avec des linguistes nous ont également amené à assembler des compilateurs permettant la description de la morphologie de l'ikota (langue bantoue) et de la sémantique de l'anglais (au moyen de la frame semantics).


Constrained Clustering by Constraint Programming (Soutenance de thèse) Chuong Duong Khanh, LIFO, Université d'Orléans

La classification non supervisée, souvent appelée par le terme anglais de clustering, est une tâche importante en Fouille de Données. Depuis une dizaine d'années, la classification non supervisée a été étendue pour intégrer des contraintes utilisateur permettant de modéliser des connaissances préalables dans le processus de clustering. Différents types de contraintes utilisateur peuvent être considérés, des contraintes pouvant porter soit sur les clusters, soit sur les instances. Dans cette thèse, nous étudions le cadre de la Programmation par Contraintes (PPC) pour modéliser les tâches de clustering sous contraintes utilisateur. Utiliser la PPC a deux avantages principaux : la déclarativité, qui permet d'intégrer aisément des contraintes utilisateur et la capacité de trouver une solution optimale qui satisfait toutes les contraintes (s'il en existe). Nous proposons deux modèles basés sur la PPC pour le clustering sous contraintes utilisateur. Les modèles sont généraux et flexibles, ils permettent d'intégrer des contraintes d'instances must-link et cannot-link et différents types de contraintes sur les clusters. Ils offrent également à l'utilisateur le choix entre différents critères d'optimisation. Afin d'améliorer l'efficacité, divers aspects sont étudiés. Les expérimentations sur des bases de données classiques et variées montrent qu'ils sont compétitifs par rapport aux approches exactes existantes. Nous montrons que nos modèles peuvent être intégrés dans une procédure plus générale et nous l'illustrons par la recherche de la frontière de Pareto dans un problème de clustering bi-critère sous contraintes utilisateur.


Prédiction de la qualité en traduction automatique : problèmes d'évaluation et limitations des systèmes supervisés Erwan Moreau, Trinity College Dublin, Ireland

Face aux difficultés rencontrées dans l'amélioration des systèmes de traduction automatique (TA) eux-mêmes, plusieurs problématiques connexes se sont développées ces dernières années. L'une d'elle vise à estimer la qualité des traductions proposées, de manière à fournir une indication qui guidera par exemple la prise de décision dans une chaîne de production : phrase à publier en l'état, à faire post-éditer, à traduire entièrement manuellement, etc. Le raisonnement est essentiellement le suivant : puisque la qualité de la TA est variable, essayons au moins de distinguer les cas où elle est satisfaisante des autres. Lancée en 2012, la "Quality Estimation Shared Task" organisée par le "Workshop on Statistical Machine Translation" fait référence dans le domaine et permet de mesurer les progrès non négligeables effectués sur la question, aussi bien en termes de méthodes que de performances. L'erreur en moyenne des valeurs absolues (Mean Absolute Error, MAE) est la principale mesure d'évaluation de tels systèmes, et logiquement aussi le critère d'optimisation de la plupart des systèmes par apprentissage supervisés. Nous montrerons que l'utilisation de cette mesure d'évaluation (pertinente au demeurant), associée au fait que les algorithmes classiques d'apprentissage supervisé dépendent beaucoup de la distribution des données d'entraînement, entraînent un biais marqué en faveur des scores de qualité "moyens". Nous identifierons d'abord ce problème expérimentalement grâce aux données de la "Quality Estimation Shared Task". A défaut d'une solution, nous proposerons différentes méthodes pour mesurer l'effet de ce biais. Enfin nous détaillerons certaines conséquences annexes à travers différentes expériences, dont l'une remet assez sérieusement en cause l'adaptation des méthodes employées par rapport à la définition du problème (ou l'inverse !). Le système utlisé dans toutes nos expériences a été conçu pour être aussi représentatif que possible que la majorité des systèmes de l'état de l'art, de sorte que nos observations soient largement généralisables. Notons finalement que le phénomène général observé pourrait ne pas être limité au cas de l'estimation de la qualité en TA, mais s'étendre à d'autres applications présentant des caractéristiques similaires.


SQL/AA : Privacy-Preserving Query Execution using a Decentralized Architecture and Tamper Resistant Hardware Benjamin Nguyen, LIFO, INSA Centre Val de Loire

Current applications, from complex sensor systems (e.g. quantified self) to online e-markets acquire vast quantities of personal information which usually ends up on central servers. Decentralized architectures, devised to help individuals keep full control of their data, hinder global treatments and queries, impeding the development of services of great interest. This paper promotes the idea of pushing the security to the edges of applications, through the use of secure hardware devices controlling the data at the place of their acquisition. To solve this problem, we propose secure distributed querying protocols based on the use of a tangible physical element of trust, reestablishing the capacity to perform global computations without revealing any sensitive information to central servers. There are two main problems when trying to support SQL in this context: perform joins and perform aggregations. In this presentation, we will detail the subset of SQL groub by queries on a sigle table and show how to secure their execution in the presence of honest-but-curious attackers. Cost models and experiments demonstrate that this approach can scale to nationwide infrastructures.


Comparaison et évolution de schémas XML (Soutenance de thèse) Joshua Amavi, LIFO, Université d'Orléans / LI, Université de Tours

XML est devenu le format standard d'échange de données. Nous souhaitons construire un environnement multi-système où des systèmes locaux travaillent en harmonie avec un système global, qui est une évolution conservatrice des systèmes locaux. Dans cet environnement, l'échange de données se fait dans les deux sens. Pour y parvenir nous avons besoin d'un mapping entre les schémas des systèmes. Le but du mapping est d'assurer l'évolution des schémas et de guider l'adaptation des documents entre les schémas concernés. Nous proposons des outils pour faciliter l'évolution de base de données XML. Ces outils permettent de : (i) calculer un mapping entre le schéma global et les schémas locaux, et d'adapter les documents; (ii) calculer les contraintes d'intégrité du système global à partir de celles des systèmes locaux; (iii) comparer les schémas de deux systèmes pour pouvoir remplacer un système par celui qui le contient; (iv) corriger un nouveau document qui est invalide par rapport au schéma d'un système, afin de l'ajouter au système. Des expériences ont été menées sur des données synthétiques et réelles pour montrer l'efficacité de nos méthodes.


Proposition de combinaison de systèmes en TAL : annotations partielles et décomposition duale Joseph Le Roux, Laboratoire d'Informatique de Paris Nord, Université Paris 13

La résolution de problèmes en TAL par combinaison de systèmes, la réalisation des fameux systèmes joints, fait désormais partie de la "trousse à outils" classique des chercheurs du domaine. Le fait de résoudre plusieurs tâches de front permet bien souvent de bénéficier d'interactions vertueuses entre les systèmes de résolution qui partagent de l'information et "s'entraident" dans leurs tâches respectives. Ceci donne souvent un avantage à ces méthodes comparées aux approches en cascade, dans lesquelles les systèmes sont chaînés séquentiellement. Dans cet exposé nous développerons une approche qui place la combinaison des solutions de systèmes élémentaires au coeur de la démarche de résolution et qui sera illustrée sur deux tâches, l'analyse syntaxique et l'étiquetage de séquences pour la segmentation des mots composés. L'idée centrale est de produire pour une tâche donnée une combinaison de systèmes "artificielle" dans le sens où cette tâche était traditionnellement résolue par un unique système. Nous produisons plusieurs systèmes similaires (par exemple des analyseurs CFG ou des étiqueteurs CRF), mais qui ne voient pas exactement les mêmes données d'entraînement. Plus précisément, nous entraînons tous les systèmes sur les mêmes corpus, mais certains types d'annotations ne seront disponibles qu'à certains systèmes, de telle sorte que les systèmes auront été effectivement entraînés sur des données différentes. Chaque système est alors considéré comme un "expert" avec une vue partielle du problème, et le but de la combinaison est de mettre d'accord ces experts. Les structures produites par les systèmes pouvant être assez différentes, surtout dans le cas des analyseurs syntaxiques, il est difficile de réaliser cette combinaison par pure programmation dynamique (les sous-calculs ne se partagent pas forcément). Cependant, il doit tout de même exister des points d'accord entre les systèmes pour arriver à un consensus. Nous proposons donc de réaliser cette combinaison en utilisant une méthode issue de l'optimisation combinatoire et de la recherche opérationnelle, la décomposition lagrangienne, qui permet d'intégrer des contraintes d'accord à un problème de recherche de meilleure solution. Nous obtenons alors des algorithmes de combinaison qui procèdent par reparamétrisations successives jusqu'à obtention de solutions compatibles avec chaque système. Expérimentalement, nous montrons que cette méthode est très performante. Pour l'analyse syntaxique, nous obtenons les meilleurs résultats à ce jour sur le "Penn Treebank" (EMNLP 2013). Nous obtenons également des résultats au-dessus de l'état de l'art pour la segmentation en mots composés sur le corpus arboré de Paris 7 (COLING 2014).


Décompositions de trigraphes Antoine Mamcarz, LIFO, Université d'Orléans

Trigraphs have been introduced by Maria Chudnovsky in 2003. They have proven to be a useful tool to handle recursive graph decompositions. Even though trigraphs have received more and more attention in the past few years, their algorithmic aspects have not been completely investigated. We will give algorithms for various decompositions of triraphs, including H-joins, modular and split decomposition, clique cutset decomposition and skew partition.


Introduction à la vérification déductive avec Frama-C Virgile Prevosto, CEA LIST

Frama-C (http://frama-c.com/) est un atelier d'analyse de code C permettant d'établir de nombreuses propriétés de programme grâce à différents greffons proposant chacun une technique particulière. Outre le langage C, Frama-C peut prendre en entrée des spécifications écrites en ACSL (ANSI/ISO C Specification Language), langage basé sur la notion de contrats de fonction. Après avoir rapidement présenté Frama-C et ses principaux greffons, nous nous concentrerons sur l'un d'entre eux, WP, qui permet de prouver la conformité d'une implantation C vis-à-vis d'une spécification ACSL, à partir de la logique de Hoare et de la génération de plus faibles pré-conditions. Plus précisément, WP génère des obligations de preuve à partir des formules ACSL, qui sont ensuite transmises à des prouveurs automatiques comme Alt-ergo. Si les prouveurs indiquent que toutes les obligations sont vraies, alors l'implantation est conforme à sa spécification. Sinon, il faut soit corriger une des deux en cas de bug avéré, soit aider les prouveurs en ajoutant des clauses ACSL intermédiaires pour obtenir des obligations de preuves plus faciles à montrer par les prouveurs. Cette activité de preuve sera illustrée par différents exemples simples de programmes munis de leur spécification.


Modélisation et implémentation de parallélisme implicite pour les simulations scientifiques basées sur des maillages (Soutenance de thèse) Hélène Coullon, LIFO, Université d'Orléans

Le calcul scientifique parallèle est un domaine en plein essor qui peut permettre d'augmenter la vitesse des longs traitements, de traiter des problèmes de taille plus importante ou encore des problèmes plus précis. Ce domaine permet donc d'aller plus loin dans les calculs scientifiques, d'obtenir des résultats plus pertinents, car plus précis, ou d'étudier des problèmes plus volumineux qu'auparavant. Dans le monde plus particulier de la simulation numérique scientifique, la résolution d'équations aux dérivées partielles (EDP) est un calcul particulièrement demandeur en ressources parallèles. Si les ressources matérielles qui permettent le calcul parallèle sont de plus en plus présentes et disponibles pour les scientifiques, à l'inverse leur utilisation et la programmation parallèle se démocratisent difficilement. Pour cette raison, des modèles de programmation parallèle, des outils de développement et même des langages de programmation parallèle ont vu le jour et visent à simplifier l'utilisation de ces machines. Il est toutefois difficile, dans ce domaine dit du "parallélisme implicite", de trouver le niveau d'abstraction idéal pour les scientifiques, tout en réduisant l'effort de programmation. Ce travail de thèse propose tout d'abord un modèle permettant de mettre en oeuvre des solutions de parallélisme implicite pour les simulations numériques et la résolution d'EDP. Ce modèle est appelé "Structured Implicit Parallelism for scientific SIMulations" (SIPSim), et propose une vision au croisement de plusieurs types d'abstraction, en tentant de conserver leurs avantages. Afin de valider SIPSim, une implémentation du modèle, sous la forme d'une bibliothèque C++ pour les architectures à mémoire distribuée, nommée SkelGIS, est également proposée dans cette thèse. SkelGIS a été implémentée pour les maillages réguliers à deux dimensions ainsi que pour les simulations sur les réseaux, qui représentent une sous partie des simulations à plusieurs phénomènes physiques. Enfin, cette thèse traite la validation de la bibilothèque SkelGIS, en terme de difficulté de programmation et en terme de performances, par la mise en place de deux cas d'application réels (en collaboration avec des mathématiciens) : une simulation complexe d'écoulement de l'eau sur les surfaces planes, ainsi qu'une simulation d'écoulement du sang dans un réseau artériel. Pour résumer, cette thèse traite du parallélisme implicite pour les simulations numériques basées sur des maillages, du modèle aux cas d'application.


Challenging machine learning classification tasks André Carlos Ponce Leon Ferreira de Carvalho, Universidade de São Paulo at São Carlos, Brazil

One of the main applications of Artificial Intelligence is data classification. Most of the data classification problems reported in the literature deal with only two classes, static classes, classes that have the same level of importance and disjunctive classes. These may be named simple classification problems. In this talk, I will discuss advanced classification problems, like multiclass classification, hierarchical classification, multilabel classification, one-class classification and novelty detection. Research results on some of these issues will be presented. Short Bio: André C. P. L. F. de Carvalho is Full Professor in the department of Computer Science, University of São Paulo, Brasil. His main research interests are data mining, data science and machine learning. Prof. de Carvalho has more than 300 peer reviewed publications, including 10 best papers awards from conferences organized by ACM, IEEE and SBC. He is a member of the International Association for Statistical Computing (IASC) Council and director of the Center of Machine Learning in Data Analysis, University of São Paulo.


A Graph Reduction Machine for Web Service Compositions Martin A. Musicante, Federal University of Rio Grande do Norte, Department of Computer Science, Natal, Brazil

Web Services are the standard for the deployment of Internet applications. Web service composition consists on combining existing web service interfaces to provide new functionality. A number of programming languages have been proposed to describe web service compositions, being BPEL the de-facto standard. Although the formal treatment of web service compositions is recurrent in the literature, the formalization of runtime systems for them is rare. In this work we introduce BP-AM, a graph reduction machine for the implementation of web service composition languages. We define (i) A set of translation functions from a BPEL-like language into graphs and (ii) A set of graph transformation rules in the form of a small-step operational semantics. The execution of a composition (program) consists on transforming its graph by using the rules of the abstract machine. A prototype implementation of BP-AM has been developed in Java. Experiments using this prototype show that service compositions run in BP-AM with performance comparable to that obtained using industrial tools. Joint work with Daniel A. S. Carvalho, Alberto Pardo and Umberto S. Costa.


Vers la construction à large couverture de la représentation du sens de phrases de langue naturelle Benoît Crabbé, Université Paris Diderot-Paris 7, INRIA Rocquencourt

Dans cet exposé, je traiterai le problème d'analyse syntaxique à large couverture de phrases de langues naturelles et de son interface avec la sémantique. Partant de l'hypothèse que la représentation du sens de phrases de langue naturelle s'appuie sur leur structure, je présenterai principalement un algorithme d'analyse syntaxique robuste lexicalisé pour CFG inspiré de GLR et qui propose une désambiguisation des hypothèses d'analyse sur base d'un modèle entièrement discriminant. Une seconde partie de l'exposé, plus succincte, présentera les grandes lignes d'un projet de recherche destiné à augmenter l'algorithme de représentations vectorielles encodant une sémantique distributionnelle.


On the Context-Freeness Problem for Vector Addition Systems Grégoire Sutre, Laboratoire LaBRI - CNRS - Université de Bordeaux

Petri nets, or equivalently vector addition systems (VAS), are widely recognized as a central model for concurrent systems. Many interesting properties are decidable for this class, such as boundedness, reachability, regularity, as well as context-freeness, which is the focus of this work. The context-freeness problem asks whether the trace language of a given VAS is context-free. This problem was shown to be decidable by Schwer in 1992, but the proof is very complex and intricate. In this work, we revisit the context-freeness problem for VAS, and give a simpler proof of decidability. Our approach is based on witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. As a corollary, we obtain that the trace language of a VAS is context-free if, and only if, it has a context-free intersection with every bounded regular language. Our approach allows us to show that the context-freeness problem for VAS, whose complexity was not established so far, is ExpSpace-complete. Joint work with Jérôme Leroux, Vincent Penelle and M. Praveen.


Les capitalistes sociaux : les sentiers de la gloire sur Twitter Nicolas Dugué, LIFO - Université d'Orléans

Les capitalistes sociaux sont des utilisateurs particuliers de Twitter. Ces utilisateurs cherchent à obtenir un maximum de followers par des méthodes que nous décrirons pour gagner de la visibilité sur ce réseau. La visibilité et la potentielle influence obtenues par ces utilisateurs ne sont pas basées sur le contenu de leurs tweets et la crédibilité de leur compte mais sur une accumulation de followers artificielle. Il est donc intéressant de détecter ces utilisateurs et d'étudier leur réel impact sur le média social.


A Linear-Time Algorithm for Computing the Prime Decomposition of a Directed Graph With Regard to the Cartesian Product Christophe Crespelle, LIP - ENS Lyon

We design the first linear-time algorithm for computing the prime decomposition of a digraph G with regard to the cartesian product. A remarkable feature of our solution is that it computes the decomposition of G from the decomposition of its underlying undirected graph, for which there exists a linear-time algorithm. First, this allows our algorithm to remain conceptually very simple and in addition, it provides new insight into the connexions between the directed and undirected versions of the cartesian product of graphs.


Design de structures d'ARN avec contraintes de séquence : une approche à base de langages formels Alain Denise, Université Paris Sud

Le problème du design (ou repliement inverse) de structures secondaires d'ARN est le suivant : la donnée est une structure cible dont on ne connaît pas la séquence. Il s'agit d'engendrer une ou des séquences qui se replieront selon cette structure. Certaines applications en biologie nécessitent d'ajouter des contraintes sur les séquences résultats, par exemple des motifs qui y sont obligatoires ou interdits. Je présenterai une méthode de résolution de ce problème fondée sur l'utilisation de grammaires formelles et d'automates finis, et comment elle a été appliquée dans le cadre d'une collaboration avec une équipe de biologie expérimentale.


Vers l'analyse statique de langages fonctionnels par réécriture et automates d'arbres Thomas Genet, IRISA, Université de Rennes

La complétion d'automates d'arbres est une technique permettant d'approcher l'ensemble des termes accessibles par réécriture. On peut voir la complétion d'automate comme une technique d'ARTMC (Abstract Regular Tree Model Checking) particulière. Si l'on code un programme fonctionnel (pur) par un système de réécriture, la complétion permet d'obtenir un sur-ensemble régulier des résultats de ce programme, i.e. une sur-approximation régulière de l'image de cette fonction. Actuellement, nous étudions l'application de ce principe à l'analyse statique de langages comme OCaml. L'objectif est de proposer un mécanisme de vérification complétant l'inférence de type d'OCaml. En donnant des propriétés régulières sur les valeurs d'entrée de fonctions simples, nous pouvons obtenir des propriétés régulières sur les résultats. Par exemple, il est possible de montrer que l'application d'une fonction filtrant les 0 sur une liste d'entiers quelconques, rend une liste d'entiers différents de de 0. Cependant, pour couvrir un sous-ensemble intéressant d'OCaml, plusieurs défis sont à relever: garantir la terminaison et la précision de l'analyse, prendre en compte les stratégies d'évaluation, prendre en compte l'ordre supérieur, prendre en compte les types built-ins, automatiser la transformation de Ocaml vers les systèmes de réécriture, etc. Concernant ces problèmes, je présenterai l'état des lieux de nos réflexions et travaux ainsi que les questions encore ouvertes.


Mesure de performance des algorithmes de routage pour le HPC Matthieu Perotin, BULL Extreme Computing R&D, Bruyères-Le-Châtel

Les réseaux haute-performance utilisés par les super-calculateurs connaissent en ce moment une évolution rapide, résultant en partie de l'apparition de nouvelles topologies spécifiques. Les algorithmes de routage qui organisent les communications sur ces "fabriques" doivent répondre à un objectif portant à la fois sur les performances applicatives mais aussi sur la résilience. Ce deuxième aspect devient critique avec l'augmentation des tailles des super-calculateurs et la "course à l'exa-flop". La littérature documente de nombreux algorithmes pour chaque type de topologie, voire pour des topologies quelconques, sans pour autant s'attarder sur leur performance effective. Cet exposé tente d'apporter une réponse à cette problématique en la considérant sous un regard: - multi-critère (de multiples fonctions objectif existent) - en-ligne (les pannes surviennent de façon non planifiée) - temps réel (des contraintes fortes existent sur les temps de réaction)


Systèmes multi-agents et culture Loïs Vanhée, Université Montpellier 2 et Universiteit Utrecht

Une des différences clé entre l'humain et l'animal est sa capacité à produire et surtout à échanger et à intégrer une vaste quantité d'information abstraites: une culture. Cette capacité pourtant apparemment simple est cruciale pour construire des phénomènes collectifs bien plus évolués: allant du langage à une structure sociale en passant par la capacité de conserver des acquis techniques. Le lien entre l'individuel et le collectif est particulièrement étudié par les systèmes multi agents, qui servira de technique de référence pour cette présentation. On verra comment l'utiliser pour effectuer des simulations de systèmes sociaux qui utilisent une culture, mais aussi comment s'inspirer de la culture pour améliorer les systèmes multi-agents.


Systèmes complexes : des réseaux génétiques à la ségrégation urbaine Eric Goles, Adolfo Ibáñez University, Santiago, Chili

On presentera des résultats de modélisation de réseaux de régulation génétiques et une famille d'automates à deux dimensions liés au problème de ségrégation de Schelling. Dans le cadre des réseaux d'origine biologique, on discutera de la robustesse du modèle du point de vue dynamique -- c'est-à-dire comment les attracteurs changent avec le mode d'actualisation du réseau. Dans le cadre du problème de ségrégation, on travaillera sur une grille bidimensionnelle où l'on caractérisera les clusters ségrégués selon un paramètre local de tolérance de chaque individu.


Several aspects of probabilistic cellular automata Damien Regnault, IBISC - Université Evry-Val d'Essonne

From the point of view of a computer scientist, deterministic cellular automata are known as a parallel computation model. Different studies have introduced randomness in this model by considering probabilistic transitions. In this talk, I will present the different motivations of these studies as well as the current results and open questions.


Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components Arnaud Lanoix, LINA, Université de Nantes

Dynamic reconfigurations increase the availability and the reliability of component-based systems by allowing their architectures to evolve at runtime. Recently we have proposed a temporal pattern logic, called FTPL, to characterize the correct reconfigurations of component-based systems under some temporal and architectural constraints. As component-based architectures evolve at runtime, there is a need to check these FTPL constraints on the fly, even if only a partial information is expected. Firstly, given a generic component-based model, we review FTPL from a runtime verification point of view. To this end we introduce a new four-valued logic, called RV-FTPL (Runtime Verification for FTPL), characterizing the “potential” (un)satisfiability of the architectural constraints in addition to the basic FTPL semantics. Potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation or satisfiability of the property under consideration. Secondly, we present a prototype developed to check at runtime the satisfiability of RV-FTPL formulas when reconfig- uring a Fractal component-based system. The feasability of a runtime property enforcement is also shown. It consists in supervising on the fly the reconfiguration execution against desired RV-FTPL properties. The main contributions are illustrated on the example of a HTTP server architecture.


Une vue d'ensemble de l'extraction Coq Pierre Letouzey, PPS - Université Paris Diderot-Paris 7

Le mécanisme d'extraction de Coq permet de transformer des preuves Coq en programmes fonctionnels. Cet exposé a pour but d'illuster le comportement de cet outil sur plusieurs définitions possibles de la division euclidienne en Coq, ainsi que sur quelques exemples plus avancés. L'extraction est ensuite décrite de manière plus générale: propriétés-clés, principaux cas d'utilisation, forces, faiblesses et perspectives.


First impressions about the use of an embedded low-power manycore processor for HPC Marcio Castro, Universidade Federal do Rio Grande do Sul (Brazil)

The exponential growth in processor performance seems to have reached a turning point. Nowadays, energy efficiency is as important as performance and has become a critical aspect to the development of scalable systems. These strict energy constraints paved the way for the development of manycore processors such as the MPPA-256, which integrates 256 cores in a single low-power chip. In this talk, I will discuss about the use of an embedded low-power manycore processor (MPPA-256) for HPC. In addition to that, I will show some of the performance and energy consumption results obtained when parallelizing a well-known irregular NP-complete problem, the Traveling-Salesman Problem (TSP), on the MPPA-256 as well as on other platforms that comprise general-purpose and low-power multicores. Finally, I will discuss about my current work in cooperation with the BRGM on porting the main kernel of a seismic wave propagation simulator on MPPA-256.


Extraction de code fonctionnel à partir de spécifications inductives Catherine Dubois, ENSIIE

Nous proposons une méthode pour extraire des contenus purement fonctionnels à partir de types inductifs logiques dans le contexte du Calcul des Constructions Inductives (CCI). Cette extraction peut se faire vers des langages fonctionnels à la ML (OCaml, Haskell) ou encore vers le CCI lui-même. Dans ce dernier cas le code fonctionnel extrait s'accompagne de la preuve de sa correction par rapport à la spécification dont il est extrait. Ces travaux (sujet principal de la thèse de Pierre-Nicolas Tollitte) ont donné lieu à un plugin Coq. Cette approche a également été adaptée de manière à synthétiser du code Focalize à partir de propriétés Focalize. La méthode mise en oeuvre s'appuie sur une analyse de consistance de mode qui permet de vérifier qu'un calcul est possible et sur l'utilisation d'une structure de données intermédiaire, le reltree, qui donne de la spécification inductive initiale une vue qui facilite la génération de code. Le processus de génération vers OCaml, Coq et Focalize est en grande partie partagé par les 2 mécanismes de génération de code fonctionnel. Travail réalisé en collaboration avec David Delahaye et Pierre-Nicolas Tollitte.