Agenda
juin
-
14:0015:00
The tree-independence number of a graph is the analogue of treewidth where, instead of minimising the size of bags, we minimise the size of a stable set contained in a bag. Chordal graphs have tree-independence 1, and it remains an active line of research to determine the tree-independence of various graph classes — or even to establish whether it is bounded in general. We show that graphs with no induced C4 nor P1+P4 have tree-independence at most 2 by proving a conjecture of Hilaire, Milanič, and Vasić (2025) stating that they can be made chordal by deleting a clique.
This is joint work with Marthe Bonamy and Sarah Houdaigoui.
Fanny Hauser (LaBRI)
Vérifiez que vous êtes bien inscrits sur le site du [gdr-ifm-gt-graphes] : [ https://gtgraphes.labri.fr/pmwiki/pmwiki.php/Equipes/Equipes#membres | https://gtgraphes.labri.fr/pmwiki/pmwiki.php/Equipes/Equipes#membres ]
Remarks / Remarques
Find all the information of the working group on this [ https://graphesetoptimisation.labri.fr/pmwiki.php/Groupe/GT?userlang=en | web page ] .
Retrouvez toutes les informations du GT sur cette [ https://graphesetoptimisation.labri.fr/pmwiki.php/Groupe/GT | page web ] .FrançaisLaBRI/178 -
14:0015:00
Le développement logiciel est un processus intrinsèquement incrémental. À cette fin, la plupart des langages de programmation fournissent aux programmeurs des mécanismes de base leur permettant d’indiquer qu’une fonctionnalité donnée n’est pas encore implémentée, par exemple au moyen d’exceptions dédiées. Malheureusement, à l’exception des vérificateurs de types incrémentaux, la plupart des outils utilisés pour raisonner sur la correction des programmes — tels que les cadres de test, d’analyse et de vérification — ne tiennent pas compte de ces idiomes d’incomplétude. En conséquence, les programmeurs sont confrontés soit à des rapports d'échec erronés, soit à la charge de modifier leurs spécifications, ce qui sacrifie le lien de causalité direct entre le code et les outils de raisonnement. Dans cette présentation, j'illustrerai ce problème dans le contexte des tests, en considérant à la fois les tests unitaires et les tests basés sur les propriétés, ainsi que la programmation certifiée dans les assistants de preuve. L'examen du problème dans des contextes aussi disparates nous permet d'isoler les concepts fondamentaux nécessaires à la construction d'outils de raisonnement véritablement incrémentaux.
Biographie :
Éric Tanter est professeur titulaire au département d'informatique de l'Université du Chili. Il a obtenu son doctorat conjointement à l'Université de Nantes et à l'Université du Chili en 2004. Ses recherches portent sur les langages de programmation et le génie logiciel, allant des fondements théoriques des langages de programmation à l'étude empirique des pratiques de programmation. Récemment, il s'est fortement impliqué dans les fondements et la pratique du typage et de la vérification graduels. Il occupe une chaire internationale de l'Inria pour la période 2025-2029.
Salle 178 (LaBRI) -
11:0012:00
Colette Johnen (LaBRI)
Title: From Static Stabilization to Dynamic Stabilization in case of bounded recurrent edges
Abstract:
We consider the problem of the Dynamic Simulation, which consists in the design of a transformer that simulates distributed algorithms in a dynamic environment modeled by a dynamic graph. We consider dynamic graphs with a fixed topology, meaning that each existing edge appears infinitely often.
We introduce a self-stabilizing transformer adapted to graphs where every edge appears at least once during τ consecutive synchronous rounds.
Our transformer is minimal in terms of hypotheses in the following sense: solving the Dynamic Simulation Problem in graphs with recurring edges either requires the knowledge of either a bound on the edge recurrency (i.e. τ
), or the knowledge on number of edges.Finally, we introduce the notion of time-bounded stabilization corresponding to pseudo-stabilizing algorithms for which an upper bound on the convergence time depending only of the network's topology.
joint work with Gabriel Le Bouder
FrançaisLaBRI 178 -
14:0015:00
Analysing Temporal Reasoning in Description Logics Using Formal Grammars
In this joint work with Anton Gnatenko and Camille Bourgaux, we establish a connection between reasoning in fragments of the temporal description logic TEL (an extension of TEL with operators from LTL) and the so-called conjunctive grammars. This allows us to close some open problem regarding the ultimate periodicity of TEL models, and the undecidability of query answering. It also provides decidability results for new interesting fragements of TEL, and paves the way towards practical reasoners.
FrançaisLaBRI -
16:0018:00
Le jury est constitué des membres suivants :
Tamara Munzner
Raimund Dachselt
Niklas Elmqvist
Caroline Appert
David Auber
Amphi LaBRI -
09:3012:00
Aymeric Ferron soutien sa thèse intitulée : « Exploration de visualisations concrètes et immersives pour communiquer l'impact environnemental des actions quotidiennes ».
Salle Ada Lovelace (Inria)
juillet
-
14:0018:00
Nina Lassale-Astis soutient sa thèse intitulée : « Développement d’une méthodologie hybride d’augmentation des données : Application à la détection de défaut supervisée en tomographie RX».
Amphi LaBRI