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
09/12/2024 : Complexité additive sur les mots avec Walnut
Pierre Popoli (Université de Liège, équipe de maths discrètes)
Résumé
25/11/2024 : Mechanisation of computation for identity types in Martin-Löf type theory
Thibaut Benjamin (University of Cambridge)
Résumé
21/10/2024 : Program Comprehension
Tomaz Kosar (Université de Maribor, Slovénie)
Résumé
Attention : Débute à 13 h 30.
21/10/2024 : Computer Science Programs at the University of Maribor
Tomaz Kosar (Université de Maribor, Slovénie)
Résumé
Attention : Débute à 14 h 45.
14/10/2024 : Distributed Depth-First Search Tree through Separator Sets
Benjamin Jauregui (Universidad de Chile (Santiago, Chile))
Résumé
23/09/2024 : Forward geochemical modeling as guiding tool for seafloor exploration
Vincent MILESI (ISTO)
Résumé
18/07/2024 : Langage de spécification et outil de vérification pour le consentement et la nécessité des données fondés sur une classification relative au respect de la vie privée
Myriam Clouet (LIFO)
Résumé
12/06/2024 : Analysis and Visualization of Blockchain Data: An Interdisciplinary Approach
Natkamon Tovanich (ÉCOLE POLYTECHNIQUE (Palaiseau))
Résumé
Attention : Débute à 09 h.
11/06/2024 : [séminaire d'équipe CA] Forward geochemical modeling as guiding tool for seafloor exploration
Vincent Milesi ()
Résumé
Attention : Débute à 11 h. Lieu : IUT B004
03/06/2024 : Programmation quantique et optimisation combinatoire
Olivier PLOTON (LIFAT, Tours)
Résumé
03/06/2024 : [Visio] Analyse affective du contenu multi-source par apprentissage profond
Mohamed Hamroun (XLIM, Université de Limoges)
Résumé
Attention : Débute à 15 h.
17/05/2024 : Reaction systems
Daniela Genova (University of Northern Florida)
Résumé
Attention : Débute à 10 h 30.
29/04/2024 : Data-Centric Machine Learning in Healthcare
Pratik Gajane ()
Résumé
23/04/2024 : Apprentissage Relationnel: La Logique et les Algorithmes remettent en cause les techniques d'apprentissage profond
Giacomo Bergami (Newcastle University)
Résumé
Attention : Débute à 10 h.
08/04/2024 : Targeting scale-out and scale-up platforms with a unified parallel programming model
Nicolo Tonci (Université de Pise)
Résumé
04/04/2024 : Optimal cybersecurity strategies based on multi-agent system verification
[Bourges et visio] Gabriel Ballot (EDF & Télécom Paris, Institut Polytechnique de Paris)
Résumé
Attention : Le séminaire sera disponible en visio : lien à venir Lieu : Salle de réunion INSA Bourges
27/03/2024 : Un problème de graphe (sommet)-coloré : le couplage maximum minimalement coloré
[Visio] Jonas Sénizergues (LABRI)
Résumé
26/03/2024 : Percolation bootstrap sur les pavages par losanges
Victor Lutfalla (Université Aix-Marseille)
Résumé
Attention : Débute à 11 h.
25/03/2024 : Présentation de la charte de mise à disposition d’un droit d’administration local pour les personnels
Baptiste Mulot (DSI Université Orléans)
Résumé
25/03/2024 : Degreewidth : a new parameter for solving problems on tournaments
[Visio] Tom Davot (Université de Glasgow)
Résumé
Attention : Débute à 15 h.
22/03/2024 : TBA
[Visio] Léa Bayati (Université d'Évry)
Résumé
Attention : Débute à 09 h.
21/03/2024 : Aller et retour : Histoire de calculs sur des graphes
Amélia Durbec (JUNIA, Lille)
Résumé
Attention : Débute à 09 h.
20/03/2024 : Empowering Data Platforms with Smart Data Modeling and Management Strategies
Matteo Francia (Université de Bologne (Italie))
Résumé
Attention : Débute à 15 h.
18/03/2024 : Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Gueneau (INRIA Saclay)
Résumé
18/03/2024 : A modular approach to automata networks
[Visio] Pacôme Perrotin (Universidade Presbiteriana Mackenzie, São Paulo, Brésil )
Résumé
Attention : Débute à 15 h.
15/03/2024 : Exact Algorithms and Lowerbounds for Multiagent Path Finding: Power of Treelike Topology
[Visio] Foivos Fioravantes (Czech Technical University, Prague)
Résumé
Attention : Débute à 10 h 30.
11/03/2024 : Covering some vertices with paths and a Hamiltonian degree condition for tough graphs
Cléophée Robin (GREYC)
Résumé
26/02/2024 : Path Covers of Temporal Graphs
Antoine Dailly (LIMOS)
Résumé
19/02/2024 : [PAMDA] A Global Approach for Optimizing Denormalized Schemas through a Multidimensional Cost Model
Jihane Mali (De Vinci Research Center)
Résumé
05/02/2024 : Énumération output-sensitive des complétions cordales minimales
Caroline Brosse (INRIA, Sophia-Antipolis)
Résumé
22/01/2024 : Effective Exploration of Graph-Structured Data
Madhulika Mohanty (INRIA, Saclay)
Résumé
15/01/2024 : [GAMoC] Computability of compact sets
Djamel Eddine AMIR (LORIA Nancy)
Résumé
08/01/2024 : MaLISSiA: Machine Learning and Interpretation of Sub-Surface Architectures
Gautier Laurent (ISTO)
Résumé
Mechanisation of computation for identity types in Martin-Löf type theory Thibaut Benjamin, University of Cambridge
Martin-Löf type theory is a powerful theory that is at the foundation of modern proof assistants such as Coq, Lean, Agda. It provides a unifying framework to formalise mathematics and software. Although this framework is powerful enough to formalise and verify very complex software (like for instance the CompCert C compiler, formally verified in Coq), its practical use is constrained by the large proof effort it requires, rendering the adoption of such tools slower. Various techniques are considered to simplify and streamline the use of proof-assistants. For instance, identity types, that represent equalities have a very rich and complex structure, and it is common to ignore that structure by adding a principle called Uniqueness of Identity Proofs (UIP). This axiom states that any two identity proofs are equal thus enforcing in a way proof irrelevance for equality. Another example is the so-called univalent axiom (originally coming from a connection with homotopy theory) that for computer scientists mean that the formalisation can be done in a way that is independent of the choice of datatypes, as long as those datatypes encode the same information. This is not only a powerful reasoning principle that allows one to reason on simple but inefficient datatypes and transport the results to finicky but efficient ones, it also reflects the very common computer science practice of hiding the implementation of datatypes under an API to make the programs more modular. Unfortunately, UIP and the univalence axiom are incompatible. In this talk, I will present a workflow that I am designing to handle and automate complex computation on identity types, in an effort to reduce the need for UIP and render practical the use of the univalence axiom. I will in particular show the implementation of this workflow as a Coq plugin, that uses a secondary tool called CaTT, which is specifically designed to handle the algebraic structure of identity types, called higher groupoid.
Program Comprehension Tomaz Kosar, Université de Maribor, Slovénie
TBA
Computer Science Programs at the University of Maribor Tomaz Kosar, Université de Maribor, Slovénie
Distributed Depth-First Search Tree through Separator Sets Benjamin Jauregui, Universidad de Chile (Santiago, Chile)
Separator sets have been utilized in algorithmic solutions for various classic problems in graph theory, including maximum matching, depth-first search (DFS), and Boolean circuits. However, their study in distributed models has been limited. In this talk, I will introduce distributed models and present the first deterministic algorithm in the CONGEST model that computes separator sets for planar graphs. Additionally, I will show how these sets can be employed to construct a DFS spanning tree in O(diam(G)) rounds, where diam(G) denotes the diameter of the graph, improving the best-known deterministic and distributed algorithm.
Forward geochemical modeling as guiding tool for seafloor exploration Vincent MILESI , ISTO
Exploration of remote areas such as Earth’s seafloor or Icy Moons in our Solar system often involves limited ‘time on target’ and no ability to return to areas of interest because of environmental, operational, and financial constraints. One way of maximizing scientific return is to achieve more knowledgeable decision-making at the time of exploration. This can be achieved by creating a framework before exploration of what to expect using modeling tools and then comparing expectations with observations in real-time.
As part of the NASA-funded project SUBSEA, I developed this approach using geochemical modeling for the exploration of the Seacliff hydrothermal vent field, seen as an Earth’s analog of Saturn’s icy moon, Enceladus. In this presentation, I will show you how forward geochemical modeling allows (1) identification of the most informative parameter to measure on the field and (2) improvement of result-informed decision making during scientific exploration. Building on this work, I would like to initiate discussions on how the multiplication of a priori mechanistic modeling could be coupled to machine learning technics to refine our predictive capabilities of remote, unexplored areas on Earth and beyond.
Langage de spécification et outil de vérification pour le consentement et la nécessité des données fondés sur une classification relative au respect de la vie privée Myriam Clouet, LIFO
La vie privée est un droit fondamental que l’on retrouve dans plusieurs lois dans le monde entier. Donc, vérifier qu’un système respecte la vie privée est crucial. Cependant, la vie privée est une notion complexe. Assurer qu’un système respecte la vie privée nécessite de vérifier que les propriétés de vie privées sont respectées durant tout le cycle de vie, ce qui complique le processus de vérification. Une grande variété de solutions ont été proposées pour améliorer le respect de la vie privée. Il est souvent difficile de précisément identifier quand elles ciblent la même problématique.
Dans cette thèse, j’adresse ces problèmes en proposant une façon de classifier des articles concernant la vie privée et une approche pour vérifier des propriétés de vie privée à deux étapes du cycle de vie. Je propose GePyR, une nouvelle représentation de la vie privée, générique et spécialisable, et une ontologie instanstiable, PyCO, qui modélise les éléments clés de la vie privée et leurs relations. Cette classification est évaluée sur la littérature, en réalisant un Systematic Mapping Study. Dans cette thèse, je formalise également deux propriétés de vie privée, la conformité aux finalités consenties et la conformité à la nécessité des données. Je propose une nouveau langage de spécification, CSpeL, qui permet de formaliser les éléments nécessaires pour vérifier ces propriétés, et introduis un nouvel outil, CASTT, pour vérifier ces propriétés sur des traces d’exécutions, sur un modèle ou un programme. Cette approche est appliquée sur deux cas d’utilisation à deux niveaux d’abstraction, pour évaluer sa correction, son efficacité et son utilité.
Lien Rendez-vous RENATER : https://rendez-vous.renater.fr/SeminaireMyriamClouet_541c39-98be55-fc3b69
Analysis and Visualization of Blockchain Data: An Interdisciplinary Approach Natkamon Tovanich, ÉCOLE POLYTECHNIQUE (Palaiseau)
Blockchain, a decentralized peer-to-peer network storing append-only transaction data, has emerged as a transformative technology with potential applications beyond cryptocurrencies like Bitcoin and Ethereum. Despite the wealth of available data, its practical applications are still evolving and not fully understood. My research adopts an interdisciplinary approach, integrating visual analytics, network science, and data mining, aiming to understand emergent user behaviors and mechanisms in the blockchain system.
In my doctoral thesis, I focused on Bitcoin mining, a critical activity to validate transactions and ensure network stability. My work included a systematic review of blockchain data visualization, algorithm development for miner identification, and empirical analyses of mining pool behaviors. I developed a visual analytics tool, MiningVis, to explore historical mining concentration and identify factors influencing miners’ behaviors.
My ongoing research addresses transaction network analysis and Decentralized Finance (DeFi) risk management. I investigate Bitcoin money flows using graph embedding techniques to differentiate user behaviors. Collaborating with economists, I develop simulations to assess systemic risks in decentralized lending protocols, aiming to create a visual analytics tool for risk detection and trend analysis.
Furthermore, I obtained a grant from CHIST-ERA to work on the FairOnChain project (Fair and Modular Blockchain Data Infrastructure for Open Science and Society). The project aims to develop a FAIR-compliant infrastructure to standardize cross-platform data APIs, facilitating effective querying, annotating, and referencing of blockchain data. The collaboration comprises four consortium partners: École Polytechnique, EPFL, HEG Genève, and Imperial College London.
[séminaire d'équipe CA] Forward geochemical modeling as guiding tool for seafloor exploration Vincent Milesi,
Exploration of remote areas such as Earth’s seafloor or Icy Moons in our Solar system often involves limited ‘time on target’ and no ability to return to areas of interest because of environmental, operational, and financial constraints. One way of maximizing scientific return is to achieve more knowledgeable decision-making at the time of exploration. This can be achieved by creating a framework before exploration of what to expect using modeling tools and then comparing expectations with observations in real-time.
As part of the NASA-funded project SUBSEA, I developed this approach using geochemical modeling for the exploration of the Seacliff hydrothermal vent field, seen as an Earth’s analog of Saturn’s icy moon, Enceladus. In this presentation, I will show you how forward geochemical modeling allows (1) identification of the most informative parameter to measure on the field and (2) improvement of result-informed decision making during scientific exploration. Building on this work, I would like to initiate discussions on how the multiplication of a priori mechanistic modeling could be coupled to machine learning technics to refine our predictive capabilities of remote, unexplored areas on Earth and beyond.
Programmation quantique et optimisation combinatoire Olivier PLOTON, LIFAT, Tours
Tout d'abord, nous décrirons les principes de la mécanique quantique et leur application à la programmation, sous le formalisme des matrices unitaires et des circuits. Puis nous exposerons quelques algorithmes quantiques célèbres, ainsi qu'un algorithme inédit d'optimisation combinatoire quantique dû à Camille Grange. Enfin, nous évoquerons la situation du quantique en pratique, et ses perspectives d’évolution.
[Visio] Analyse affective du contenu multi-source par apprentissage profond Mohamed Hamroun, XLIM, Université de Limoges
Ce séminaire se penche sur l'exploration novatrice de l'analyse affective du contenu multi-source à travers l'apprentissage profond, en mettant en lumière son application dans le domaine médical. L'examen se concentre sur la richesse des données multi-source, provenant de réseaux sociaux, d'imagerie médicale, de dossiers patients, et d'autres sources hétérogènes, et leur potentiel dans la prédiction des maladies telles que la dépression, la maladie
d'Alzheimer, le diabète, le cancer, et même les maladies infectieuses comme le COVID-19.
En mettant l'accent sur les méthodes d'analyse avancées, nous explorons comment ces données peuvent être utilisées pour prédire, détecter et prévenir ces maladies. Notre objectif est d'illustrer les progrès récents dans ce domaine passionnant et d'explorer comment ces avancées peuvent améliorer les stratégies de diagnostic, de prévention et de traitement, ouvrant ainsi de nouvelles perspectives pour la santé publique et la médecine personnalisée.
Reaction systems Daniela Genova, University of Northern Florida
TBA
Data-Centric Machine Learning in Healthcare Pratik Gajane,
The data-centric approach has recently gained prominence in artificial intelligence and machine learning. In particular, data-centric machine learning holds significant potential in the healthcare domain due to the availability of vast amounts of data. In this presentation, we will first briefly explore the advantages of employing data-centric machine learning in healthcare. Following that, we will delve into the challenges associated with the effective utilization of data-centric approaches in this field. Afterward, I will describe my ongoing and future work in some of these challenges, namely: effective and fair use of data, explainable data analysis, adapting ML solutions to diverse datasets, and use of heterogeneous data.
Visio : https://teams.microsoft.com/l/meetup-join/19%3ameeting_MGE4NjM3MTItYTQ2Ny00MzMwLTg2ZmUtZjFjNTg1ZTA1NjYy%40thread.v2/0?context=%7b%22Tid%22%3a%22967236d1-9003-4f1a-9556-8afe047945f1%22%2c%22Oid%22%3a%222dec3a6b-b16b-4d61-8656-9a3c31f51e03%22%7d
Apprentissage Relationnel: La Logique et les Algorithmes remettent en cause les techniques d'apprentissage profond Giacomo Bergami, Newcastle University
L’utilisation toujours croissante de l’apprentissage automatique pour extraire des modèles qui peuvent être utilisés dans le monde réel met en question les techniques d’apprentissage profond. Pour ces algorithmes, les explications peuvent être connu depuis cet apprentissage et jamais pendant l’apprentissage même, ce met en question leur infaillité: par exemple, la validation clinique d’un modèle nécessite qu’un clinicien vérifie que le modèle appris ne contredit pas la littérature médicale. Donc, je présente KnoBAB, une base de connaissances temporelle qui utilise des approches d'apprentissage et de vérification formelle plus similaires à l'apprentissage relationnel. Ceci permet de générer des traces temporelles conformes à un modèle, d'effectuer une vérification formelle des traces temporelles, et d'obtenir des modèles de conformité temporelle à partir de la séquence d'événements temporels. Cela garantit la définition d’algorithmes de apprentissage automatique avec garanties. Nous contextualisons cette recherche dans le domaine médical. En marge, je montre mes travaux sur l'intégration de données dans le domaine médical, ainsi que ceux sur les algorithmes pour les graphes de propriétés.
Lien pour le séminaire : https://teams.microsoft.com/l/meetup-join/19%3ameeting_MjBkZjc0OTgtZDYxMC00ZDMyLWI5MGQtMzhkMDRjN2JkMTYx%40thread.v2/0?context=%7b%22Tid%22%3a%22967236d1-9003-4f1a-9556-8afe047945f1%22%2c%22Oid%22%3a%222dec3a6b-b16b-4d61-8656-9a3c31f51e03%22%7d
Targeting scale-out and scale-up platforms with a unified parallel programming model Nicolo Tonci, Université de Pise
The proliferation of interconnected devices, capable of generating huge amounts of data, requires highly performing applications to extract insights. These needs amplify the demand of new scalable algorithms and programming interfaces, both for shared-memory and distributed-memory architectures. Currently, the standard tools to approach this challenge are either too complex or unflexible for programmers. This talk aims to present a new distributed-memory run-time system for FastFlow’s building-blocks. FastFlow is a C++ structured parallel programming library, originally targeting shared-memory platforms. This new support allowed the exploitation of the parallel resources of multiple interconnected machines. The main target of the proposed run-time system was to enable an easy and smooth transition between shared-memory FastFlow applications to equivalent distributed-memory ones. A preliminary analysis of the new run-time system reported considerable benefits from the programmability and flexibility points of view. Furthermore, it's presented MTCL, a multi-transport communication library, employed by the distributed RTS of FastFlow. Along with the tools, some applications are shown as well.
Optimal cybersecurity strategies based on multi-agent system verification [Bourges et visio] Gabriel Ballot, EDF & Télécom Paris, Institut Polytechnique de Paris
Cybersecurity is a context in which at least two agents, namely a defender and an attacker, interact to achieve conflicting objectives. As such, its analysis with game theory is natural. Most game theoretic approaches for cybersecurity rely on analytical games described by a reward function depending on agent actions, and the goal is often to find equilibriums (e.g, Nash equilibrium). However, these techniques imply a new analysis for each particular system or network. Contrarily, defining Multi-Agent System (MAS) formalisms adapted to describe multi-step attacks can help generically design defense systems. Moreover, model checking defender strategic abilities in the MAS offers guarantees on active cyber defenses leveraged by the security team, including honeypots (i.e, deception mechanisms) and Moving Target Defenses (i.e, system reconfiguration). The existing formalisms do not capture all the aspects of active defenses, so we developed Capacity Alternating-time Temporal Logic to reason about strategic abilities under imperfect information of the agents’ capacities.
Lien Zoom : https://zoom.us/j/93056321213?pwd=d2JkMG5tQnNYM2FqU3U2VVFxanNkQT09
Un problème de graphe (sommet)-coloré : le couplage maximum minimalement coloré [Visio] Jonas Sénizergues, LABRI
Le problème du couplage maximal est un problème de graphe classique, connu pour se résoudre en temps polynomial. Lorsqu'on ajoute des couleurs sur les sommets et des contraintes de couleurs sur la solution, de maximisation ou de minimisation par exemple, comment les choses évoluent-elles ?
Percolation bootstrap sur les pavages par losanges Victor Lutfalla, Université Aix-Marseille
La percolation bootstrap est un phénomène de contamination locale depuis une configuration initiale tirée aléatoirement classiquement étudiée sur la grille carrée ZZ^2.
Nous allons présenter la généralisation de ce phénomène aux pavages par losange et présenter la preuve que pour tout paramètre p>0, lorsque l'on tire une configuration initiale tirée aléatoirement selon une distribution de Bernoulli de paramètre p sur un pavage de Penrose, la probabilité que cette configuration percole (c'est à dire que tout le pavage soit contaminé par la percolation bootstrap) est de 1.
Présentation de la charte de mise à disposition d’un droit d’administration local pour les personnels Baptiste Mulot, DSI Université Orléans
Dans le contexte de l’application de la Politique de Sécurité des Systèmes d’Information de l’Etat (PSSIE - N°5725/SG), il est exigé de limiter l’utilisation du compte d’administration local des postes de travail informatique aux équipes en charge de l’exploitation et du support de ces postes.
L’utilisation des privilèges d’administration doit être réalisée uniquement pour les actions le nécessitant, pour installer des logiciels pédagogiques par exemple. Les utilisateurs ne doivent ainsi disposer que des privilèges nécessaires à la réalisation des actions relevant de leur mission.
Conscient que cette exigence de sécurité ne doit pas entraver le bon fonctionnement de l’établissement, la DSI a mis en place une charte de mise à disposition d’un compte d’administration local.
Celle-ci permet de définir un cadre respectant les obligations de la PSSIE tout en garantissant la flexibilité nécessaire à la réalisation des missions des agents.
Degreewidth : a new parameter for solving problems on tournaments [Visio] Tom Davot, Université de Glasgow
We define a new parameter for tournaments called degreewidth. The degreewidth of a tournament T denoted by Delta(T) corresponds to the minimum k such that we can order the vertices of T such that every vertex is incident to at most k backward arcs, i.e. for such arcs the head is before the tail w.r.t this order. Thus, a tournament is acyclic if and only if its degreewidth is zero. Additionally, the class of sparse tournaments defined by Bessy et al. corresponds to tournaments with degreewidth one. Therefore, this parameter can be seen as a measure of how far the tournament is from being acyclic.
We first study computational complexity of finding degreewidth. Namely, we show it is NP-hard and complement this result by a 3-approximation algorithm. We also provide a cubic algorithm to decide if a tournament is sparse.
Finally, we study classical graph problems Dominating Set and Feedback Vertex Set parameterized by degreewidth. We show the former is fixed parameter tractable whereas the later is NP-hard on tournaments of degreewidth one. Additionally, we study Feedback Arc Set on sparse tournaments.
TBA [Visio] Léa Bayati, Université d'Évry
TBA
Aller et retour : Histoire de calculs sur des graphes Amélia Durbec, JUNIA, Lille
De nombreux systèmes dynamiques discrets sont influencés par le graphe sur lequel ils opèrent. Dans le cas des réseaux d'automates, il existe un lien fort entre les propriétés de la dynamique (existence et nombre de points fixes, longueur des transients) et des propriétés très étudiées en théorie des graphes : la forte connexité et l'existence de cycles pairs. La largeur arborescente est classiquement connue pour avoir une forte influence sur la complexité de différents problèmes. On peut conjecturer que celle-ci pourrait avoir une forte influence sur la Turing-complétude dans les sous-shifts de graphes.
Nous pouvons également nous intéresser à ce qu'il se passerait si nous laissions la dynamique évoluer la structure du graphe sur laquelle elle s'opère. De tels objets, appelés dynamiques causales de graphes, sont la source d'une multitude de questions. Outre leur intérêt en physique théorique où ils permettent d'apporter des éléments de réponse à des questions en cosmologie et dynamique des fluides en tant que modèle physique, ces dynamiques pourraient également apporter des algorithmes parallélisables pour des problèmes classiques en informatique.
Empowering Data Platforms with Smart Data Modeling and Management Strategies Matteo Francia, Université de Bologne (Italie)
Data platforms are advanced and distributed information systems that manage the entire data lifecycle through ecosystems of services glued and automated by metadata. Creating effective data platforms requires addressing several issues, including (i) choosing appropriate services based on the data processes to support, (ii) finding data representations that are flexible enough to store heterogeneous data and enable efficient queries, (iii) defining querying systems to query data distributed in different engines, and (iv) leveraging meta-data for automated and smart management. Such challenges must be tackled by techniques and methodologies involving different stakeholders (e.g., designers, end users, cloud service providers) and must be tested on real case studies to understand their real power. This is of particular interest following the increasing interest in digital transformation (e.g., the Agritech sector) fueled by the ever-increasing data generated by more and more pervasive systems.
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C Armaël Gueneau, INRIA Saclay
In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI).
In this talk, I will present our first steps towards the goal of developing program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C.
Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.
A modular approach to automata networks [Visio] Pacôme Perrotin, Universidade Presbiteriana Mackenzie, São Paulo, Brésil
Predicting the limit dynamics of automata networks (like deciding if a given network has a fixed point) is a hard problem. We would like to improve our understanding of their attractors on specific families of networks, like disjunctive networks. To do so, we decompose networks into modules, which were defined in my PhD thesis; these modules are automata networks with inputs and outputs. In this presentation we will show what has been done so far using this modular approach, including the definition of output functions (a new way of understanding a network's computation) and an equivalence to the fixed points of a family of cellular automata, culminating in the showcase of a interaction digraph transformation method that's in the works, and could help to prove the dynamical equivalence of families of networks through the transformation of their interaction digraphs.
Exact Algorithms and Lowerbounds for Multiagent Path Finding: Power of Treelike Topology [Visio] Foivos Fioravantes, Czech Technical University, Prague
In the Multiagent Path Finding (MAPF) problem, we focus on efficiently finding non-colliding paths for a set of k agents on a given graph G, where each agent seeks a path from its source vertex to a target. An important measure of the quality of the solution is the length of the proposed schedule l, that is, the length of a longest path (including the waiting time).
In this work, we propose a systematic study under the parameterized complexity framework. The hardness results we provide align with many heuristics used for this problem, whose running time could potentially be improved based on our Fixed-Parameter Tractability (FPT) results. We show that MAPF is W[1]-hard with respect to k (even if k is combined with the maximum degree of the input graph). The problem remains NP-hard in planar graphs even if the maximum degree and the makespan l are fixed constants. On the positive side, we show an FPT algorithm for k+l.
As we continue, the structure of G comes into play. We give an FPT algorithm for parameter k plus the diameter of the graph G.
Finally, we show that the MAPF problem is W[1]-hard for cliquewidth of G plus l while it is FPT for treewidth of G plus l.
Covering some vertices with paths and a Hamiltonian degree condition for tough graphs Cléophée Robin, GREYC
A graph G is Hamiltonian if it exists a cycle in G containing all vertices of G exactly once. A graph G is t-tough if, for all subsets of vertices S, the number of connected components in G − S is at most |S| / t.
In 1973, Chvàtal conjecture the following : There exists a constant t such that every t-tough graphs is Hamiltonian.
Let t be a positive integer. A graph G with degree sequence d_1,d_2,…,d_n is P(t) (t being a positive integer) If for all i, t ≤ i < n/2, d_i ≤ i ⇒ d_{n−i+t} ≥ n−i. In 1995, Hoàng conjecture the following : If G is t-tough and P(t) then G is Hamiltonian. Hoàng prove that it is true for t ≤ 3. In 2023, Hoang and Robin proved that it is also true for t ≤ 4 by extending the Closure Lemma due to Bondy and Chvàtal into a version for tough graphs.
We prove that it is true for t≤7. To do so, we prove a lemma about covering some vertices of a graph with a bounded number of paths.
This is joint work with Chình T. Hoàng and Paul Dorbec.
Path Covers of Temporal Graphs Antoine Dailly, LIMOS
A famous result by Dilworth on posets implies that computing a minimum-size path cover (a collection of paths such that every vertex is in some path) of a directed acyclic graph (DAG) is polynomial. Those algorithms have been studied since the 1950s and are still the subject of recent improvements due to applications in fields such as bioinformatics or computational logic. Inspired by the problem of Multi-Robot Path Finding, we translate the problem on temporal graphs, that is, graphs whose arc-set changes over discrete time-steps (we say that a temporal graph is a temporal DAG/tree/etc if the underlying graph, using the union of all arcs that appear, is a DAG/tree/etc). A temporal path, in such a setting, is a path in the underlying (di)graph such that the arcs appear in strictly increasing time-steps (a robot cannot traverse multiple edges at the same time). We are interested in two problems: Temporal Path Cover (TPC), where we aim to simply cover the vertices of the temporal graph using temporal paths; and Temporally Disjoint Path Cover (TD-PC), where we want to cover the vertices with the added condition that two paths cannot occupy the same vertex at the same time, thus representing a partition by using the time-steps as a new dimension allowing paths to use the same vertex at different times (for when robots occupy the whole vertex when traversing it, for example). In both cases, we want to minimize the size of the cover. We prove that the two problems are NP-hard on temporal DAGs, even with strong constraints on both the underlying DAG and the time-steps. However, on temporal trees, while TD-PC remains NP-hard, TPC can be solved in polynomial-time. This is obtained by creating an auxiliary graph expressing the temporal connectedness of vertices, exhibiting an equivalence between temporal paths in the temporal graph and cliques in the auxiliary graph, and proving that the auxiliary graph is weakly chordal, allowing us to use powerful algorithms from the literature. Both problems are also polynomial-time solvable on temporal rooted directed trees and temporal lines, which is not the case of all problems on temporal graphs (such as Linkage). We also give an XP algorithm for TPC and an FPT algorithm for TD-PC, both parameterized by the treewidth plus the total number of time-steps. On the structural side, we discuss on when a temporal analogue of Dilworth's theorem holds in the classes that we study.
[PAMDA] A Global Approach for Optimizing Denormalized Schemas through a Multidimensional Cost Model Jihane Mali, De Vinci Research Center
As the volume of data continues to grow, the complexity of database systems has surged, giving rise to NoSQL systems. This forces Information Systems (IS) architects to constantly adapt their data models (i.e., the structure of stored information) and meticulously select the optimal option(s) for data storage and management. In response to this challenge, we propose an automated global approach for guiding the transformation of data models. Our approach initiates by transforming the conceptual model into a logical data model, then applies refinement rules recursively to generate all possible data models. To reduce the search space, our approach employs a heuristic that avoids redundancies and considers the use case.
Additionally, we propose a cost model, enabling the comparison of generated data models at a logical level. This cost model integrates both data model and query costs, along with considerations for environmental impact, financial, and time costs. For the first time, our approach introduces a multidimensional cost model that evaluates time, environmental, and financial constraints. This cost model eases the comparison of data models, helping with the selection of the most suitable one for a given use case and context by optimizing either the environmental impact or the stability of the data model.
Énumération output-sensitive des complétions cordales minimales Caroline Brosse, INRIA, Sophia-Antipolis
Minimal chordal completions of a graph, also called minimal triangulations, are an important object in graph theory. For some applications, e.g. to databases, it is useful to generate all minimal chordal completions of a graph as efficiently as possible. However, for efficiency we need to take into account the large (possibly exponential) number of solutions. This long-lasting problem was successfully addressed in 2017: Carmeli, Kenig, and Kimelfeld designed an efficient algorithm for the listing of all minimal chordal completions of a graph. Its total running time is polynomial in the number of solutions. However, for more efficiency, we aim at designing an algorithm running with polynomial delay: the time needed between two consecutive outputs should be polynomial in the input size only.
In this talk, I will present a new enumeration algorithm for the minimal chordal completions of a graph, running with polynomial delay and exponential space. After that, the space usage will be addressed, and I will exhibit how to modify our algorithm so that it only needs polynomial space.
Effective Exploration of Graph-Structured Data Madhulika Mohanty, INRIA, Saclay
Large Graphs such as YAGO, DBPedia, and Wikidata, form the backbone for many applications including chatbots, personal assistants and question answering systems. Graph database (GDB) users typically use structured queries to precisely express their information needs. However, given the exact match semantics of these languages, a common challenge that they face is that of getting empty or too few results. In this talk, I will discuss some solutions that enable GDB users to explore unfamiliar graphs. First, we integrate connecting tree patterns (CTPs) with existing graph query languages like GPML, SPARQL or Cypher, leading to Extended Queries (EQs). This allows finding general connections between two or more groups of nodes in a graph, without the need to specify exactly how. I will then present an efficient algorithm to evaluate the CTPs. Further, I will introduce Spec-QP, a system that performs automatic reformulations on user queries and efficiently evaluates them. I will conclude my talk with some ongoing works and future research directions.
[GAMoC] Computability of compact sets Djamel Eddine AMIR, LORIA Nancy
The topological properties of a set have a strong impact on its
computability properties. A striking illustration of this idea is given
by spheres and finite graphs without endpoints: if a set X is
homeomorphic to a sphere or a such graph, then any algorithm that
semicomputes X in some sense can be converted into an algorithm that
fully computes X. In other words, the topological properties of X enable
one to derive full information about X from partial information about X.
In that case, we say that X has computable type. Those results have been
obtained by Miller and Iljazović in the recent years.
We give a characterization of finite simplicial complexes having
computable type using a local property of stars of vertices. Moreover,
the reduction to homology implies that the computable type property is
decidable, for finite simplicial complexes of dimension at most 4. We
argue that the stronger, relativized version of computable type, is
better behaved. Consequently, we obtain characterizations of strong
computable type, related to the descriptive complexity of topological
invariants. This leads us to investigate the expressive power of low
complexity invariants in the Borel hierarchy and their ability to
differentiate between spaces. Notably, we show that they are sufficient
for distinguishing finite topological graphs.
MaLISSiA: Machine Learning and Interpretation of Sub-Surface Architectures Gautier Laurent, ISTO
This seminar will present an original approach to artificial intelligence application in geosciences, as proposed in the MaLISSiA project.
Artificial intelligence and digital twins offer tremendous opportunities for modelling and understanding Earth systems. However, these new developments have mainly been applied to geophysical processes occurring within relatively well-constrained geometries (e.g., on earth surface) and they have yet to make a breakthrough in the characterization of sub-surface architectures. Yet these geometrical considerations are determinant in the localization of sub-surface Earth processes. The difficulty to access sub-surface causes paramount epistemic uncertainties, which result in peculiar scientific challenges, e.g., the dependencies to scale, to time, and a general lack of observation with respect to the complexity of structures. These limitations are generally counterbalanced by expert interpretations that rely on human learning from analogues (outcrops and simulations). The search for more formal and automated solutions is challenging both the formalization of geological knowledge and the development of innovative artificial intelligence methods.
The MaLISSiA project draws its inspiration from the geocognitive process developed by human learning and interpretation. It proposes a new paradigm for automatically interpreting and explaining sub-surface architectures. This paradigm is based on two founding components: (1) a formalisation of geological and interpretation concepts in dedicated ontologies; (2) a Geocognitive Interpretation Process that breaks a complex spatial data assimilation problem into a series of explanation proposal and testing. Such formalism also enables the training of machine learning algorithms to answer key questions in the process. This training calls for the development of a corpus of interpreted geological references, based on both natural objects and process-based simulations that reproduce geological history.
Université d'Orléans | INSA Centre Val de Loire