• Summary
• LIFO Members (Directory)
• Research Teams
• CA
• GAMoC
• LMV
• Pamda
• SDS
• Research Actions
• Doctoral Research
• Seminars and Events
• Seminars (french)
• Events at LIFO
• Events out of LIFO
• Publications and Software
• Publications
• Doctoral and Habil. Theses
• Research Reports
• Software
• Technology transfer

• Contacts/Reaching LIFO
• Who's who at LIFO
• Coming to LIFO
• Teaching
• CS Department
• CS Technical Department
• INSA Centre-Val de Loire

Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37

LIFO seminars (french)

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

27/03/2023 : [LMV] Une caractérisation impérative des algorithmes (multi-)BSP
Frédéric Gava (Université Paris-Est Créteil) Résumé
Attention : Débute à 13 h 30.

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

[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] 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.