- Renseignements pratiques
- Enseignement
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).
15/12/2021 : [Séminaire CA] Representation Learning based constrained clustering : applications to tabular and multi-variate time series data
Dino Ienco (UMR TETIS, INRAE)
Résumé
Attention : Débute à 10 h 30.
15/12/2021 : [Soutenance de thèse] Clustering et intégration de connaissances
Viet Dung Nghiem Nguyen (LIFO, Université d'Orléans)
Résumé
Attention : Lieu : Amphi H, bâtiment 3IA
13/12/2021 : Neo4Tourism – Un framework pour l’analyse de la mobilité et de la circulation touristique sur une base de données graphe
Nicolas Travers (ESILV)
Résumé
22/11/2021 : Améliorer un lecteur d’écran
Pierre Réty (LIFO, Université d'Orléans)
Résumé
19/10/2021 : [Séminaire CA] L'apprentissage profond multimodal
Vincent Nguyen (LIFO, Université d'Orléans)
Résumé
Attention : Débute à 10 h. Lieu : Salle SR3, bâtiment 3IA
14/10/2021 : [Séminaire SDS] E-voting protocols - how to analyse the security of these (real-world) systems?
Alexandre Debant (Inria Nancy)
Résumé
Attention : Les informations de connexion sont disponibles dans le canal Séminaires du groupe Teams / Débute à 15 h 15. Lieu : Zoom
23/09/2021 : [Séminaire SDS] Sécurité des dispositifs médicaux connectés : une première étude des communications sans fil
Matthieu Bannwarth ()
Résumé
Attention : Les informations de connexion sont disponibles dans le canal Séminaires du groupe Teams / Débute à 13 h 40. Lieu : Zoom
13/09/2021 : Abundant Extensions
Henning Fernau (Université de Trèves, Allemagne)
Résumé
17/05/2021 : L'Inclusion-Exclusion pour l'ordonnancement
Olivier Ploton (Université de Tours, LIFAT)
Résumé
Attention : Lieu : En ligne
22/03/2021 : Algorithmes distribués pour la détection de sous-graphes
Ioan Todinca (Université d'Orléans, LIFO)
Résumé
Attention : Lieu : En ligne
15/03/2021 : Specification and Verification of High-Level Properties with MetAcsl
Nikolai Kosmatov (Thales Research & Technology (TRT))
Résumé
Attention : Lieu : En ligne
08/03/2021 : Online Testing of Dynamic Reconfigurations w.r.t. Adaptation Policies
Frédéric Dadeau & Olga Kouchnarenko (Univ. Bourgogne Franche-Comté, CNRS, FEMTO-ST Institute)
Résumé
Attention : Lieu : En ligne
22/02/2021 : Learning Sparse Penalties for Change-point Detection using Max Margin Interval Regression
Toby Hocking (Northern Arizona University)
Résumé
Attention : Débute à 16 h 05. Lieu : En ligne
15/02/2021 : Systèmes auto-adaptatifs: introduction et modélisation formelle par des systèmes de réécriture de graphe
Cédric Eichler (INSA Centre Val de Loire, LIFO)
Résumé
Attention : Lieu : En ligne
08/02/2021 : A calculus of Branching Processes
Jean Krivine (IRIF)
Résumé
Attention : Lieu :
01/02/2021 : Categorifying Non-Idempotent Intersection Types
Federico Olimpieri (LIPN)
Résumé
Attention : Lieu : En ligne
18/01/2021 : Toward Safe and Efficient Reconfiguration with Concerto
Simon Robillard et Hélène Coullon (IMT Atlantique)
Résumé
Attention : Débute à 13 h 45. Lieu : En ligne
Résumés des séminaires
[Séminaire CA] Representation Learning based constrained clustering : applications to tabular and multi-variate time series data Dino Ienco, UMR TETIS, INRAE
Huge amount of data are nowadays produced by a large and disparate family of sensors. While the collected information depicts static scenarios, it can be organized as tabular (or propositional) data, conversely when the information is characterized by temporal or temporal dynamic, it can be profitably structured as multi-variate time series. Collect enough labelled samples to set up supervised analysis for such kind of data is challenging while, a reasonable assumption is to dispose of a limited background knowledge that can be injected in the analysis process. In this context, constrained (or semi-supervised) clustering methods represent a well suited tool to get the most out of such reduced amount of knowledge.
In this talk I will tackle the problem of semi-supervised clustering under the lens of representational learning with modern deep learning strategies. More in detail, background knowledge (under the shape of constraints) is exploited to modify the original data representation with the aim to use available, standard and largely recognized clustering algorithms (i.e. K-means).
To this end, after a general introduction, I will present two recent research works (we have developed in my research team) in which representational-based semi-supervised clustering algorithms were developed to deal with propositional as well as multi-variate time series data.
[Soutenance de thèse] Clustering et intégration de connaissances Viet Dung Nghiem Nguyen, LIFO, Université d'Orléans
Le clustering sous contraintes (une généralisation du clustering semi-supervisé) vise à exploiter les connaissances des experts lors de la tâche de clustering. La connaissance s'exprime souvent par un ensemble de contraintes et peut prendre des formes diverses. Dans cette thèse, nous développons deux mécanismes pour intégrer des contraintes dans la tâche de clustering. Dans la première partie, nous proposons une méthode déclarative post-traitement pour adapter la sortie d'un algorithme de clustering pour satisfaire les contraintes. L'originalité est de considérer une matrice d'allocation qui donne les scores d'attribution des points à chaque cluster et de trouver la meilleure partition satisfaisant toutes les contraintes. Dans la deuxième partie, nous proposons un cadre unifié pour intégrer les contraintes générales dans un modèle de clustering avec l'apprentissage profond. La généricité se représente en formalisant des contraintes en logique et en considérant leurs modèles. Les résultats expérimentaux sur des jeux de données connus montrent que notre approche est compétitive avec d'autres méthodes spécifiques aux contraintes tout en étant générale. De plus, nous avons défini et formulé de nouveaux types de contraintes en clustering : la contrainte de couverture de cluster limitant le nombre de clusters auxquels un groupe de points peut appartenir, et la contrainte d'équité combinée prenant en compte à la fois l'équité de groupe et l'équité individuelle.
Neo4Tourism – Un framework pour l’analyse de la mobilité et de la circulation touristique sur une base de données graphe Nicolas Travers, ESILV
Les traces numériques laissées par les utilisateurs actifs sur les réseaux sociaux sont devenues un moyen populaire d'analyser le comportement des touristes. La grande quantité de données générées par les touristes constitue un indicateur clé pour comprendre leur comportement en fonction de divers critères. Les analyses des déplacements des touristes ont un rôle crucial dans le marketing touristique pour construire des outils d'aide à la décision pour les offices de tourisme. Ces acteurs sont confrontés à la nécessité de discerner la circulation des touristes de manière quantitative et qualitative.
Ce travail présente la construction du framework Neo4Tourism d’analyse de la circulation à l’aide d’une base de données orientée graph : Neo4j. Avec une approche base de données, nous sommes à même de définir des transformations du graphe en y associant des aspects géodésiques et cartographiques, qui ont pour but de produire de nouveaux graphes utiles pour les étapes d’analyse. Nous proposons ensuite de nouvelles approches d’analyse de la circulation touristique basées sur la centralité ou la propagation intégrant cette dimension géodésique, mais également les manipulations multiéchelles. Nous avons pu tester notre approche sur les données provenant de Tripadvisor à l’échelle nationale.
Ces travaux de recherche ont été effectués au DVRC, en convention avec les métropoles de Bordeaux et Lille, ainsi qu’un partenariat avec le laboratoire EIREST de Paris 1 Panthéon Sorbonne.
Nicolas Travers est professeur d'informatique à l'école d'ingénieurs ESILV, Paris la Défense. Au laboratoire DVRC, il est le responsable du groupe Digital, dédié à l'analyse numérique dans les domaines de l'informatique, management des SI et du marketing digital. Il a obtenu sa thèse de doctorat en informatique à l’UVSQ en 2006 et son habilitation (HDR) de l'Université de la Sorbonne en 2018. Ses principaux sujets portent sur la gestion et l'optimisation des bases de données, dans des environnements distribués comme les bases NoSQL, ainsi que sur la conception de bases de données ad hoc comme le tourisme numérique (BD graph), les partitions musicales (BD XML et Search Engine) ou les bibliothèques multimodales (Document Store).
Améliorer un lecteur d’écran Pierre Réty, LIFO, Université d'Orléans
Un lecteur d’écran est un logiciel qui permet de naviguer et d’agir sur les éléments graphiques sans regarder l’écran, et restitue les textes sous forme audio ou braille. Il permet ainsi aux personnes en difficulté de lecture (mal-voyants, analphabètes, dyslexiques) d’utiliser l’ordinateur ou le smartphone. Un lecteur d’écran appelé VoiceOver est disponible en natif et gratuitement sur les produits Apple. Mais il présente des anomalies et des limitations. Nous cherchons ici à corriger les principaux défauts de VoiceOver, ce qu’Apple ne fait pas, en relevant plusieurs défis. Comment améliorer :
- un logiciel à sources fermées ?
- la synthèse vocale ?
- la navigation ?
Nous apportons des réponses à ces questions, ainsi qu’une implémentation. Une démonstration sera effectuée.
[Séminaire CA] L'apprentissage profond multimodal Vincent Nguyen, LIFO, Université d'Orléans
Dans ce séminaire, je présenterai mes thèmes de recherche en mettant l'accent sur l'apprentissage multimodal (fusion multimodale, alignement multimodal, traduction multimodale, etc.)
2 travaux en apprentissage multimodal sur 2 applications différentes sont présentés. La première application concerne la fusion multimodale pour apprendre des caractéristiques multimodales de documents (bande dessinée) qui sont ensuite utilisés pour le regroupement et la recherche d'objets. La seconde application concerne la traduction multimodale où une modalité est traduite en une autre modalité (de l'image au texte).
[Séminaire SDS] E-voting protocols - how to analyse the security of these (real-world) systems? Alexandre Debant, Inria Nancy
For many years, e-voting protocols have been designed and formal methods (computational or symbolic) have been developed to prove the main properties that such systems must satisfy, e.g. vote secrecy and verifiability. Based on these security proofs, e-voting systems are now used (or ready to be) in our daily life for association elections, company elections, or even political elections (e.g. in Switzerland, Estonia, Australia…).
In this talk I will first introduce the topic of e-voting and how symbolic models can be used to provide security proofs. Then, I will discuss the accuracy of the models with respect to the real-world constraints that arise when these protocols are deployed in practice. To this aim, I will present new attacks we discovered. Finally, I will talk about some properties (e.g. cast-as-intended, accountability) which are at the limit of the state-of-the-art in symbolic analysis.
[Séminaire SDS] Sécurité des dispositifs médicaux connectés : une première étude des communications sans fil Matthieu Bannwarth,
Durant son stage, Mathieu a mis en place une plateforme de pentesting sans fil (RF) dans le but d'étudier certains aspects sécuritaires des communications non filaires des implants médicaux connectés (IOMT). Cette plateforme a vocation à identifier/reproduire des vulnérabilités existantes/nouvelles.
Après une rapide revue de littérature des vulnérabilités déjà connues sur certains implants, potentiellement capable de faire courir un risque médical ou pour les données personnelles du patient, Mathieu présentera les premières analyses et résultats qu'il a pu obtenir. Après une prise en main de la plateforme sur du matériel IOT non médical, Mathieu a pu entreprendre des tests sur un implant médical donné. Mathieu présentera les premiers résultats obtenus, et les limites de diverses natures qui ont freiné l'avancée des travaux.
Mots clés : Pentesting, RF (Radio Fréquence), Objets connectés, Implants, Médical, Données personnelles, Vulnérabilités, Failles de sécurité.
Abundant Extensions Henning Fernau, Université de Trèves, Allemagne
Most algorithmic techniques dealing with constructing solutions to combinatorial problems build solutions in an incremental fashion.
Often, the whole procedure could be visualized by means of a search tree.
To the leaves of such a search tree, we can associate solutions, while to the inner nodes, only pre-solutions can be associated.
By looking at all leaves of the search tree, an optimum solution can be found if desired.
In particular for reasons of speed, it is crucial to prune off potential branches of the search tree by deciding at an early stage if a certain pre-solution
can be ever extended to a solution that is optimal. But, how easy is it to tell if such pruning is possible?
In this survey, we first present a motivating example as an introduction, followed by a general framework for extension problems. Then we show that such problems are really abundant, and these examples also prove that the complexity of these extension problems can be the same as or different from that of the original combinatorial question.
L'Inclusion-Exclusion pour l'ordonnancement Olivier Ploton, Université de Tours, LIFAT
Cette présentation est consacrée à l'application de l'Inclusion-Exclusion aux problèmes d'ordonnancement NP-difficiles. Ce sont des problèmes d'optimisation dans lesquels on alloue dans le temps des ressources à des travaux, sous contraintes et en minimisant un critère. L'Inclusion-Exclusion est une technique combinatoire permettant de dénombrer les solutions d'un problème sans les énumérer explicitement. On peut l'utiliser pour compter le nombre de solutions du problème de décision associé à tout problème d'optimisation, et en déduire un algorithme exact pour résoudre le problème d'optimisation avec une complexité pire cas modérément exponentielle en temps et pseudo-polynomiale en espace. Dans cette présentation, nous passons en revue l'Inclusion-Exclusion et certaines de ses extensions, et nous montrons comment l'appliquer pour concevoir des algorithmes exponentiels de pointe en matière d'ordonnancement.
Mots-clefs: Ordonnancement; Algorithmes exponentiels; Inclusion-Exclusion.
Algorithmes distribués pour la détection de sous-graphes Ioan Todinca, Université d'Orléans, LIFO
Basé principalement sur des travaux réalisés avec Pierre Fraigniaud (IRIF, CNRS/Univ de Paris), Pedro Montealegre (Univ. Adolfo Ibañez, Santiago, Chili), Denis Olivetti (Univ. Freiburg) et Ivan Rapaport (Universidad de Chile), présentés à DISC 2017 (International Symposium on Distributed Computing).
Un cadre classique pour le calcul distribué est le modèle LOCAL, formé d’un réseau de noeuds ayant chacun un identifiant unique et possédant ses propres données. La communication se fait de façon synchrone, lors d'une ronde de communication chaque noeud échange des messages avec ses voisins. Nous nous intéressons particulièrement au modèle CONGEST, ayant une faible bande passante : la taille des messages est d’ordre logarithmique par rapport au nombre de noeuds du réseau. L’objectif est de résoudre un problème -- par exemple de vérifier une propriété du réseau -- en un faible nombre de rondes, si possible en temps constant.
Je commencerai par une introduction au modèle CONGEST, avec ses possibilités et ses limites. Nous verrons qu’il est difficile de vérifier certaines propriétés pourtant très locales, comme la détection d’un cycle à quatre sommets, et ce même avec des protocoles probabilistes.
En revanche nous verrons qu’il est possible de vérifier en un nombre constant de rondes si le réseau possède comme sous-graphe un arbre donné. Je présenterai en détails le protocole probabiliste pour la détection d’un chemin de longueur k, étonnamment simple. J’évoquerai ensuite la façon de l’étendre à un arbre, de le rendre déterministe, et quelques autres conséquences. A travers cet exemple je m’efforcerai d’illustrer certaines problématiques et outils du calcul distribué.
Specification and Verification of High-Level Properties with MetAcsl Nikolai Kosmatov, Thales Research & Technology (TRT)
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult
to assess them. To address this issue, we propose a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in several case studies. This talk gives an overview of various contributions related to MetAcsl.
The corresponding results were published at TACAS 2019, TAP 2019 and FormaliSE 2021 (to appear). This work is a joint work with Virgile Robles, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies. Adaptation policies are seen as artifacts that describe desirable behavior of the system without enforcing a specific one. An adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their respective utility. The adaptation policy has to be faithfully implemented by the system, especially w.r.t. the priority occurring in the rules, which are generally specified for optimizing some extra-functional properties (e.g. minimizing resource consumption).
In this context, this presentation will present a model-based testing approach which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. In the end, the relative frequencies of the reconfigurations are measured in order to determine if the adaptation policy is faithfully implemented. We will illustrate our approach by simulations for a platoon of autonomous vehicles.
Joint work by Frédéric Dadeau, Jean-Philippe Gros and Olga Kouchnarenko
Learning Sparse Penalties for Change-point Detection using Max Margin Interval Regression Toby Hocking, Northern Arizona University
In segmentation models, the number of change-points is typically chosen using a penalized cost function. In this work, we propose to learn the penalty and its constants in databases of signals with weak change-point annotations. We propose a convex relaxation for the resulting interval regression problem, and solve it using accelerated proximal gradient methods. We show that this method achieves state-of-the-art change-point detection in a database of annotated DNA copy number profiles from neuroblastoma tumors.
The paper.
Systèmes auto-adaptatifs: introduction et modélisation formelle par des systèmes de réécriture de graphe Cédric Eichler, INSA Centre Val de Loire, LIFO
Les systèmes distribués modernes évoluent dans des contextes soumis à évolutions auxquelles ils doivent s'adapter. Ils doivent ainsi faire face à l'arrivée ou au départ de composants, aux pannes, aux évolutions des besoins... L'informatique autonome fournit un cadre pour la délégation de la gestion de ces (auto-)adaptations au système lui-même, limitant ou éliminant les interventions humaines.
Ce séminaire introductif présentera dans un premier temps l'informatique autonome, son inception, ses objectifs, sa mise en œuvre au travers de la boucle de contrôle MAPE-K, ainsi que quelques unes des problématiques qui lui sont associées.
Dans un second temps, nous présenterons une approche de modélisation formelle de systèmes auto-adaptatifs basée sur la réécriture de graphe. Cette approche permet de représenter l'état d'un système, ses états acceptables et ses adaptations. Finalement, nous verrons comment cette approche permet de spécifier des adaptations préservant nécessairement la correction d'un système.
A calculus of Branching Processes Jean Krivine, IRIF
(joint work with Thomas Ehrhard (CNRS, IRIF) and Ying Jiang (ISCAS, China)
CCS-like calculi can be viewed as an extension of classical automata with communication primitives. In this talk I will show what we obtained when we applied this principle to tree-automata: a calculus of branching processes (termed CBP), where the continuations of communications are allowed to branch according to the arity of the communication channel. I will show that CBP can be “implemented” by a fully compositional LTS semantics. I will argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology à la CCS and calculi with dynamic connectivity such as the π-calculus.
Reference: A Calculus of Branching Processes. Ehrhard, Krivine and Jiang. TCS 807(6) pp 169–184.
Categorifying Non-Idempotent Intersection Types Federico Olimpieri, LIPN
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
Toward Safe and Efficient Reconfiguration with Concerto Simon Robillard et Hélène Coullon, IMT Atlantique
For large-scale distributed systems that need to adapt to a changing environment, conducting a reconfiguration is a challenging task. In particular, efficient reconfigurations require the coordination of multiple tasks with complex dependencies. We present Concerto, a model used to manage the lifecycle of software components and coordinate their reconfiguration operations. Concerto promotes efficiency with a fine-grained representation of dependencies and parallel execution of reconfiguration actions, both within components and between them. In this paper, the elements of the model are described as well as their formal semantics. In addition, we outline a performance model that can be used to estimate the time required by reconfigurations, and we describe an implementation of the model. The evaluation demonstrates the accuracy of the performance estimations, and illustrates the performance gains provided by the execution model of Concerto compared to state-of-the-art systems.
Keywords: reconfiguration, component-based models, coordination, parallelism, distributed software
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 