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

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


05/07/2023 : [LMV] Une caractérisation impérative des algorithmes (multi-)BSP
Frédéric Gava (Université Paris-Est Créteil) Résumé

04/07/2023 : [PAMDA] Managing spatial and image data using modern storage and data processing environments
Cristina Aguiar (Prof invitée (São Paulo em São Carlos)) Résumé

26/06/2023 : Cybersecurity Research Results and Projects
Marko Holbl (Université de Maribor, Slovénie) Résumé

15/06/2023 : [GT Orléans Le Mans] S parser is better: one step closer to word embedding interpretability
Simon Guillot (Université du Mans) Résumé
Attention : Débute à 10 h.

09/06/2023 : [LMV] Pratique professionnelle de git
Julien Tesson (Nomadic Labs) Résumé
Attention : Lieu : Salle SR3, bâtiment 3IA

05/06/2023 : [Keynote CA] Disproving XAI Myths with Formal Methods -- Initial Results
Joao Marques-Silva (Toulouse (IRIT CNRS ANITI )) Résumé

30/05/2023 : [Keynote GAMoC] ENSnano: a geometry-based 3D modelling software for designing complex DNA nanostructures
Nicolas Schabanel (ENS LYON - CNRS) Résumé

22/05/2023 : [CA] Validation statistique de résultats expérimentaux : au-delà de la p-value, la statistique bayésienne
Aymeric Beauchamp (Equipe CA LIFO) Résumé
Attention : Lieu : Espace Com, bâtiment 3IA

17/05/2023 : [LMV] Formalisation pour la sécurisation d'applications critiques
Thierry Lecomte (Clearsy) Résumé

15/05/2023 : [Séminaire GAMOC] Calculus of constructions: at the foundation of Coq
Dieter Spreen (Université de Siegen, Allemagne) Résumé

18/04/2023 : [LMV] Analyse de boucle par quantification sur les itérations
Simon Robillard (Université de Montpellier) Résumé
Attention : Débute à 10 h 30. Lieu : Salle SR3, bâtiment 3IA

17/04/2023 : [Keynote] Déduction automatique
Simon Robillard (Université de Montpellier) Résumé
Attention : Débute à 13 h 30.

12/04/2023 : [LMV] Une approche sous-structurelle des déformations temporelles
Adrien Guatto (Université Paris Cité, IRIF) Résumé
Attention : Débute à 10 h 30. Lieu : Salle SR3, bâtiment 3IA

22/03/2023 : [PAMDA] Adéquation algorithme architecture pour l’accélération de méthodes d’inversion de données en grande dimension
Nicolas Gac (CentraleSupélec) Résumé
Attention : Débute à 13 h 30.

20/03/2023 : [PAMDA] Comment connaître le monde en ne parlant qu'à ses voisins?
Sylvie Delaët (TBA) Résumé
Attention : Débute à 13 h 30.

06/03/2023 : [Séminaire doctorant LIFO] Approches basées sur l'espace latent pour l'explicabilité des modèles de sous-titrage d'images.
Sofiane ElGuendouze (LIFO - CA) Résumé
Attention : Débute à 13 h 30.

27/02/2023 : [PAMDA] Scientific Workflow Provenance: Querying and Annonymization
Khalid Belhajjame (Paris Dauphine) Résumé
Attention : Débute à 13 h 30.

13/02/2023 : [Keynote] Frama-C, une plateforme open-source d'analyses de programmes C
Julien Signoles (CEA) Résumé
Attention : Débute à 13 h 30.

01/02/2023 : [PAMDA] Voyager dans les données : trouvailles, intérêts, langages… et au delà
Patrick Marcel (LIFAT) Résumé

23/01/2023 : [LMV] Contribution to the Analysis of the Design-Space of a Distributed Transformation Engine
Jolan Philippe (IMT Atlantique) Résumé

17/01/2023 : [PAMDA] Leveraging possibilities towards energy efficiency for computing systems, from large to small scale systems
Issam Raïs (Norvège) Résumé
Attention : Débute à 15 h.

Résumés des séminaires


[LMV] Une caractérisation impérative des algorithmes (multi-)BSP Frédéric Gava, Université Paris-Est Créteil
Après un bref rappel du modèles BSP et de sa version hiérarchique qu'est Multi-BSP, nous tenterons de répondre (formellement) à une question d'apparence naïve : qu’est-ce qu’un algorithme (multi-)BSP ? Pour ce faire, nous étendrons à BSP la définition axiomatique des algorithmes séquentiels de Gurevich, Celle-ci se base sur les algèbres évolutives aussi appelées ASMs. Avec ces nouveaux postulats, nous obtenons alors la classe des algorithmes BSP. Puis nous donnerons une équivalence algorithmique entre les algorithmes BSP et un mini langage impératif prouvant que les langages de programmation BSP usuels sont algorithmiquement complet. Nous serons alors à même de définir ce qu’est un algorithme Multi-BSP et sa caractérisation impérative. Nous terminerons par une discussion sur les limites de cette caractérisation impérative et du modèle Multi-BSP. N.B. : Aucune connaissance préalable sur les ASMs n'est nécessaire pour suivre cet exposé.


[PAMDA] Managing spatial and image data using modern storage and data processing environments Cristina Aguiar, Prof invitée (São Paulo em São Carlos)
Conventional data, such as data of numeric, alphanumeric, and date types, have a total order relation and, therefore, can be sorted and searched using ordinary relational operators (i.e., <, ≤, >, ≥). However, a crescent number of applications require managing more complex data to support a range of queries that cannot be answered using only conventional data. Among these complex data, the spatial and image data types distinguish themselves. Points, lines, and regions usually represent spatial data, while feature vectors and attributes for similarity search represent image data. Managing the spatial and image data types imposes several challenges, such as appropriate forms of storage, indexing structures, and efficient query processing. For instance, the image data type has no total order relation and cannot be sorted and searched using ordinary relational operators. Instead, images are compared through similarity. First, feature extractors process the images to generate feature vectors. Then, a distance function produces a similarity measure to determine the dissimilarity between two images based on their feature vectors. In this talk, Cristina Aguiar will present her recent research on managing spatial and image data considering solid state drives, parallel and distributed data processing frameworks, and non-conventional data warehousing environments. She will also detail how to store images in warehouses and efficiently process analytical queries extended with similarity search over images in Spark.


Cybersecurity Research Results and Projects Marko Holbl, Université de Maribor, Slovénie
Cybersecurity refers to the practices and technologies to protect digital networks, devices, and data from unauthorised access or attack. As society becomes more digitally interconnected, the importance of cybersecurity increases. In this seminar, we will present recent research results in the field of cybersecurity, including authentication and key agreement protocols in wireless body sensor networks, cybersecurity education and training, cybersecurity management and models of privacy and disclosure on social networking sites from the University of Maribor, Faculty of Electrical Engineering and Computer Science. The results presented are linked to ongoing or finished European and national projects. Additionally, current and future research directions will be discussed, focusing on browser fingerprinting and alternative authentication methods.


[GT Orléans Le Mans] S parser is better: one step closer to word embedding interpretability Simon Guillot , Université du Mans
Les modèles d'embedding de mots parcimonieux (SPINE, SINr) sont conçus pour projeter le lexique dans un espace aux dimensions interprétables. Une dimension interprétable est telle qu'un humain peut interpréter les relations sémantiques (ou syntaxiques) entre les mots actifs pour une dimension. Ces modèles sont utiles pour des tâches critiques en traitement automatique du langage naturel (par exemple, le TAL médical ou juridique) et les applications en humanités numériques. Les travaux présentés lors de ce séminaire tendent vers l'extension de l'interprétabilité au niveau du vecteur en intégrant des contraintes psycholinguistiques à la définition des représentations. Un critère clé d'un modèle interprétable est la parcimonie : pour être interprétable, tous les mots ne doivent pas être représentés par toutes les dimensions du modèle, en particulier si les humains doivent interpréter ces dimensions et leurs relations. Cela soulève une question : dans quelle mesure la parcimonie est-elle viable sur le plan des performances ? Nous introduisons donc une procédure pour augmenter la parcimonie des modèles et évaluer son impact sur deux méthodes interprétables (SPINE et SINr) afin de tendre vers une interprétabilité du vecteur. Nous introduisons également la stabilité comme nouveau critère d'interprétabilité.


[LMV] Pratique professionnelle de git Julien Tesson, Nomadic Labs
Gestion d'un code source de grande taille avec git : l'exemple de Tezos.


[Keynote CA] Disproving XAI Myths with Formal Methods -- Initial Results Joao Marques-Silva, Toulouse (IRIT CNRS ANITI )
For more than a decade, the advances in machine learning (ML) have been absolutely remarkable. However, the deployment of ML models is still impaired by lack of trust on how the best-performing ML models make predictions. The issue of lack of trust is even more acute in uses of ML models in high-risk or safety-critical domains. eXplainable artificial intelligence (XAI) is at the core of ongoing efforts for delivering trustworthy AI. Unfortunately, XAI is riddled with critical misconceptions, that foster further distrust instead of contributing to build trust. This paper highlights some of the most visible misconceptions in XAI, and shows how formal methods have been used, both to disprove those misconceptions, but also to devise practically effective alternatives.


[Keynote GAMoC] ENSnano: a geometry-based 3D modelling software for designing complex DNA nanostructures Nicolas Schabanel, ENS LYON - CNRS
Joint work with Nicolas Levy (LIP, ENS de Lyon), Allan Mills (CBS, U. Montpellier), Julie Finkel (CBS), Gaëtan Bellot (CBS) Since the 1990s, increasingly complex nanostructures have been reliably obtained out of self-assembled DNA strands: from ``simple'' 2D shapes to 3D gears and articulated nano-objects, and even computing structures. The success of the assembly of these structures relies on a fine tuning of their structure to match the peculiar geometry of DNA helices. Various softwares have been developed to help the designer. In this talk, we introduce our new software ENSnano which aim at conciliating the different approaches of preexisting softwares by providing a slick fast-responding interface combining live-editable 2D and 3D views together with new concepts to help the designer. Furthermore we will present new paradigms to design DNA origamis with arbitrary 3D curvatures. These paradigms are now part of ENSnano software and we have used them to create increasingly complex curvy DNA nanostructures with high yield and with high accuracy. These structures were evaluated by atomic force microscopy (AFM), negative stain transmission electronic microscopy (TEM), and cryogenic electron microscopy (3D cryoEM). Finally, the self-assembly of such structures remains a mystery that we will discuss at the end of talk.


[CA] Validation statistique de résultats expérimentaux : au-delà de la p-value, la statistique bayésienne Aymeric Beauchamp, Equipe CA LIFO
Dans le domaine du machine learning, le recours à des tests statistiques pour valider des résultats expérimentaux est une pratique courante. Cependant cette validation a très souvent recours au calcul de la valeur p, sujette à des problèmes d'interprétation et dont l'utilisation abusive est régulièrement critiquée par les statisticiens. Cet exposé va revenir sur les problèmes que pose la p-value avant de présenter les avantages de l'analyse bayésienne qui permet une interprétation beaucoup plus claire des résultats et de leur importance statistique, ainsi qu'un tutoriel d'utilisation d'une librairie Python dédiée à la comparaison de classifieurs.


[LMV] Formalisation pour la sécurisation d'applications critiques Thierry Lecomte, Clearsy

Le développement d'applications sûres et sécuritaires requiert une large palette de techniques pour leur développement logiciel et matériel, ainsi que pour leur vérification/validation. L'exposé présente une solution technologique (https://www.clearsy.com/outils/clearsy-safety-platform/) combinant un certain nombre de techniques, formelles ou non, comme:

  • la redondance matérielle et applicative,
  • la preuve de modèles formels,
  • la génération de code et la compilation diversifiée,
  • le passage dans un état puits restrictif en cas d'anomalie de fonctionnement.

L'approche permet de prendre en compte les défaillances aléatoires et systématiques (norme EN5012{6, 8, 9}) dans un cadre sûr (préservation de la vie humaine) et doit être étendu pour garantir la sécurité (préservation des secrets) dans un cadre sécuritaire (normes CC, IEC62433).

L'exposé fait le point sur le cadre d'application (incluant les spécifications système), le retour d'expérience, les travaux de recherche et développement en cours ainsi les problèmes scientifiques et techniques ouverts. Les thématiques couvertes incluent, à des degrés divers: la modélisation formelle, la génération de code et la compilation, la preuve mathématique, le deep-learning et la cybersécurité, le tout sous le prisme de la certification normative.


[Séminaire GAMOC] Calculus of constructions: at the foundation of Coq Dieter Spreen, Université de Siegen, Allemagne
The calculus of constructions is one of the most powerful higher-type systems of constructive logic, on which the popular proof assistant Coq is based. It consists of three logical levels; Proofs — Propositions — Kinds, Kinds are the types of operations, i.e. constructions of propositions. Prop is one such kind: the kind of all propositions, i.e. operations without input. A model construction for the calculus therefore involves giving meaning to proofs, propositions, and kinds, respectively, in such a way that the rules of the calculus hold. In the project we will give such construction by using certain order structures, known as domains. The model will avoid foundational problems that appear when collections get too large. We will show that the objects of the construction, in particular the operations, are computable.


[LMV] Analyse de boucle par quantification sur les itérations Simon Robillard, Université de Montpellier
Cette présentation décrit un cadre théorique pour analyser et vérifier des programmes contenant des boucles. Cette technique est basée sur un language de premier ordre et utilise des "expressions étendues" qui permettent de décrire à la fois les propriétés fonctionnelles et les propriétés temporelles des boucles. Elle permet, en conjonction avec des prouveurs automatiques de théorèmes existants, d'automatiser des tâches telles que la vérification de la correction partielle, la vérification de la terminaison, et la génération d'invariants pour les boucles.


[Keynote] Déduction automatique Simon Robillard, Université de Montpellier
Les systèmes informatiques occupent un rôle toujours croissant dans nos sociétés, et les défauts dans la conception ou l'implémentation de ces systèmes peuvent avoir des conséquences coûteuses. L'abstraction mathématique peut être utilisée pour obtenir des garanties fortes sur ces systèmes. Ces techniques, regroupées sous le terme de méthodes formelles, sont largement comprises et encouragées depuis plus de 50 ans, mais jusqu'à récemment, la complexité des systèmes à vérifier a empêché leur application à grande échelle. Aujourd'hui, les techniques de déduction automatique fournissent une réponse de plus en plus efficace à ce défi. Des outils ciblant diverses logiques peuvent être utilisés pour raisonner au sujet de problèmes mathématiques. Les problèmes issus de la vérification logicielle et matérielle sont, par leur nature, particulièrement adaptés au raisonnement automatique. Dans cette présentation, je donnerai un aperçu des différents outils de déduction automatique, et leur application à des problèmes de vérification.


[LMV] Une approche sous-structurelle des déformations temporelles Adrien Guatto, Université Paris Cité, IRIF
Travail mené en collaboration avec Christine Tasson et Ada Vienot. La programmation fonctionnelle réactive traite de structures de données infinies parcourues à un rythme fixé. Ce rythme doit être identique pour tous les producteurs et tous les consommateurs d'une même structure. Dans cet exposé, je présenterai un langage théorique dont les types décrivent ces rythmes de parcours, et dont la gestion sous-structurelle des contextes assure l'accord des producteurs et des consommateurs.


[PAMDA] Adéquation algorithme architecture pour l’accélération de méthodes d’inversion de données en grande dimension Nicolas Gac , CentraleSupélec
L'amélioration constante de la résolution des instruments parallèlement à la complexité croissante des méthodes de reconstruction basées sur des modèles de plus en plus précis, s'accompagne d'un besoin croissant en puissance de calcul. Les cartes accélératrices composées de GPU ou de FPGA sont une opportunité pour réduire l'écart technologique entre les systèmes d'acquisition et de reconstruction. Dans le contexte particulier de la résolution de problèmes inverses mal posés, mes travaux de recherche en adéquation algorithme-architecture au sein du Groupe Problème Inverse (GPI) du laboratoire L2S visent à prendre en compte, en amont de la définition des méthodes, le potentiel et les limites des architectures d'accélération. Après une présentation du parallélisme offert par les architectures GPU et FPGA, le contexte algorithmique des méthodes bayésiennes et leur application en reconstruction tomographique sera présenté avec un focus sur l'accélération des opérateurs de projection/rétrojection utilisés en tomographie. Le projet ANR Dark-era portant sur l’accélération des calculs pour la radioastronomie sera ensuite présenté ; ce travail collaboratif vise à construire un outil de prototypage rapide fournissant des simulations exascale des futur serveurs HPC nécessaire au traitement « temps réel » du flux de données massif du radiotélescope SKA. Enfin, des perspectives sur ces travaux seront exposées.


[PAMDA] Comment connaître le monde en ne parlant qu'à ses voisins? Sylvie Delaët, TBA
L’algorithmique répartie (distributed computing aurait dit Shakespeare) est un vaste domaine du parallélisme dans lequel on rencontre des algorithmes qui résistent aux pannes transitoires de manière optimiste : les algorithmes auto-stabilisants (self-stabilizing algorithms). Au cours de cet exposé nous aborderons quelques concepts des algorithmes répartis auto-stabilisants et nous répondrons à plusieurs questions : - De quel parallélisme parle t-on lorsqu’on aborde les algorithmes répartis auto-stabilisants ? - Est-il possible de détecter des pannes transitoires ? - Comment connaître le monde en ne parlant qu’à ses voisins ? - Peux t-on garantir par construction l’auto-stabilisation de certains algorithmes répartis ? Ces questions nous amèneront ensemble à en poser d’autres qui ouvriront, j’espère, vers des minutes de réflexion ou des années d’études...


[Séminaire doctorant LIFO] Approches basées sur l'espace latent pour l'explicabilité des modèles de sous-titrage d'images. Sofiane ElGuendouze, LIFO - CA
Le sous-titrage d'images est la tâche qui vise à générer des descriptions textuelles à partir de représentations d'images. Cette tâche nécessite l'utilisation de modèles composés basés sur l'apprentissage profond (DL), tels que CNN+LSTM ou des architectures basées sur des transformeurs. La grande complexité de ces modèles conduit souvent à considérer leur fonctionnement interne comme des boîtes noires, empêchant l'utilisateur de comprendre leur processus de décision. Malgré le large éventail de leurs domaines d'application, les systèmes de sous-titrage d'images souffrent toujours d'un manque d'interprétabilité, la plupart des travaux récents se concentrant principalement sur la génération de cartes à chaleur montrant l'importance au niveau du pixel, mais négligeant l'étude des composants de l'architecture elle-même. L'espace de représentation est un élément clé des modèles DL, la compréhension de cet espace et de la façon dont l'information est codée constitue une approche intéressante pour le DL interprétable, ce qui permet d'isoler et d'identifier l'importance de chaque composant de l'architecture impliquée dans le pipeline de sous-titrage (au moyen de perturbations gaussiennes). Les résultats de notre approche montrent que la partie visuelle, principalement composée de l'encodage visuel et du mécanisme d'attention, est plus déterminante que la partie linguistique, ce qui pourrait conduire à des explications plus subtiles. Ce travail est ensuite suivi par un protocole d'explication approfondi en concevant et en comparant deux méthodes d'explication avec des portées différentes (basée sur la substitution et basée sur la rétropropagation), au niveau de l'espace latent de la composante visuelle. Les résultats montrent que les deux méthodes obtiennent des résultats comparables et que leur portée n'a pas d'impact explicite sur la qualité des explications.


[PAMDA] Scientific Workflow Provenance: Querying and Annonymization Khalid Belhajjame, Paris Dauphine
Automated workflows have been shown to facilitate and accelerate the exploration and analysis of scientific data in many scientific fields, including life sciences and biodiversity. Provenance information, recorded during the execution of workflows, has a number of applications, for example, to facilitate the interpretation of results provided by the execution of workflows, and to better understand the validity of results and/or verify their reproducibility. In this talk, I will present our results in the context of workflow provenance management. In doing so, I will focus on two topics, namely querying and anonymizing workflow results. Regarding the first topic, we have shown that provenance querying can be performed efficiently by leveraging the workflow definition, which acts as a succinct schema, to avoid unnecessary joins when traversing the provenance graph. Regarding anonymization, we have shown how the classical k-anonymization technique can be generalized to fit the nature of the collected provenance information, and we propose an efficient algorithm to perform anonymization considering the requirements of the modules (or more precisely their providers). We conclude our talk by presenting the perspectives of our work in the area of workflow provenance management.


[Keynote] Frama-C, une plateforme open-source d'analyses de programmes C Julien Signoles, CEA
Cet exposé présentera Frama-C, une plateforme open-source dédiée à l'analyse de programmes écrits en langage C. Après un aperçu général de la plateforme, nous introduirons ses principaux greffons d'analyse. Ainsi, nous expliquerons d'abord comment prouver l'absence de comportements indéfinis (ou les détecter s'il y en a) à l'aide d'Eva, le greffon d'analyse de valeurs par interprétation abstraite, nous introduirons ensuite comment prouver des propriétés fonctionnelles à l'aide du greffon WP dédié à la vérification déductive, puis nous présenterons comment détecter des erreurs avancées en cours d'exécution d'un programme, à l'aide d'E-ACSL, le greffon dédié à la vérification à l'exécution. Enfin, nous montrerons quelques usages plus avancés combinant différentes analyses. Les différentes techniques présentées seront illustrées à travers différents exemples réels provenant de domaines applicatifs variés (nucléaire, avionique, carte à puce, ...).


[PAMDA] Voyager dans les données : trouvailles, intérêts, langages… et au delà Patrick Marcel, LIFAT
Cette présentation est un panorama des recherches menées depuis quelques années au LIFAT autour du thème général de l’exploration interactive de données. Dans une première partie, nous préciserons le problème de l’exploration interactive de données en nous attardant notamment sur (1) une définition que nous en avons donnée et (2) les mesures d’intérêt couramment utilisées dans ce cadre. Nous illustrerons brièvement quelques-une des applications que nous avons proposées, avec un focus sur l’extraction automatique de trouvailles de comparaison dans des bases de données relationnelles. Finalement nous inscrirons ces travaux dans un cadre déclaratif pour l’exploration de données que nous avons défini. Pour conclure, quelques perspectives seront évoquées.


[LMV] Contribution to the Analysis of the Design-Space of a Distributed Transformation Engine Jolan Philippe, IMT Atlantique
The design space for defining a distributed model transformation engine is a large spectrum of possibilities and opportunities to enhance performances in terms of computation time and memory consumption. Depending on the adopted decisions, the use of a transformation engine can be completely different (e.g., an incremental solution for an often-modified model vs a formally specified engine for reasoning, not performing). Already existing solutions propose engines with different goals based on several approaches including distribution, laziness, incrementality, and correctness. However, comparing the solutions is not trivial, and does not necessarily make sense. That is why we have implemented a new engine, integrating variability, that allows an analysis of its design space. From a language that has formal specifications, we created SparkTE, a parametrizable and distributed transformation engine on top of Spark. In this thesis, we aim at analysing the impact of the choices at different levels: the used programming models for defining expressions; the different semantics used to define the computation of a transformation; and the impact of engineering choices.


[PAMDA] Leveraging possibilities towards energy efficiency for computing systems, from large to small scale systems Issam Raïs, Norvège
Energy efficiency is now a recognized challenge for computing systems. Every computing system is involved in the reduction or augmentation of the overall energy consumption and global carbon emission. There are multiple ways to modulate the energy consumed by a computing system. However, taking decisions carelessly can lead to an augmentation of the energy consumption and to a disruption of existing constraints. This last statement is true for large scale computing systems (like supercomputers and clouds) but also for small scale systems (like Wireless Sensor Networks and Cyber-Physical Systems, especially when deployed in resource constrained environments). This talk gives an overview of my contributions in these two previous contexts. It also presents an overview of my current and future works.