Évènements

The k-Edge-Connected Subgraph problem and the k-Connectivity Augmentation problem are among the most basic Network Design problems and, consequently, have been heavily studied. Due to their approximation hardness, the gold standard in terms of approximation guarantee are strong constant factors. Interestingly, this approximation hardness does not carry over to planar graphs. In particular, the 2-Edge-Connected Subgraph problem admits a PTAS on planar graphs. However, the used techniques are very different from the celebrated Baker’s framework, which is a standard way to design PTASs for planar graphs. The main obstacle of using Baker’s technique in its classical form is that it requires a certain locality of the problem. However, k-edge/vertex-connectivity are global properties. We present a novel, and arguably clean, way to extend Baker’s framework to deal with larger connectivity requirements. Based on this, we obtain a PTAS for the k-Edge-Connected Subgraph problem and its vertex analog, even with costs, as long as the max-to-min cost ratio is bounded by a constant. Moreover, together with further insights, we obtain a PTAS for the k-Connectivity Augmentation problem in the same cost setting. We complement this with an NP-hardness result for planar augmentation, showing that all our results are essentially tight. This is joint work with Vera Traub and Rico Zenklusen.

Dans cet exposé, je parlerai des méthodes récentes développées par A. Elveis-Price, W. Fang, B. Louf et M. Walner pour déterminer les comportements asymptotiques des solutions de récurrences bivariées. Ces méthodes se basent sur une approche d'abord heuristique qui permet de déterminer la forme de l'asymptotique, puis dans un second temps on utilise des arguments issus des marches aléatoires dans le quart de plan pour obtenir des équivalents. On verra comment ces méthodes peuvent s'appliquer au cas des nombres de Hurwitz monotones, que l'on a étudié avec B. Louf et si le temps le permet, aux généralisations possibles.

In the era of big data, information retrieval (IR) plays a central role in how information is accessed and consumed. Recent advances in Transformer-based neural models have substantially improved retrieval performance. Two major paradigms have emerged in this context: learned sparse retrieval, which represents texts using weighted vocabulary terms, and generative retrieval, which formulates retrieval as the generation of a document identifier. While both approaches have shown strong performance, they also exhibit important limitations. Sparse retrieval methods are often constrained by the fixed vocabulary of the underlying language model, limiting their adaptability, whereas generative retrieval methods rely on arbitrary document identifiers that tend to generalize poorly to unseen documents. In this thesis, we explore how these two paradigms can be combined to obtain more efficient and more effective retrieval representations. Our core idea is to construct sparse retrieval vocabularies from learning rather than from predefined lexical tokens. We first propose REFERENTIAL and HotBERT to investigate the use of hierarchical structured identifiers as the vocabulary representation for retrieval, whose coarse-to-fine representation is designed to capture global semantics at higher levels and progressively refine finer-grained distinctions. While this representation proves expressive and effective, our analysis reveals that directly learning and optimizing hierarchical identifiers is challenging in practice. Motivated by this observation, we introduce SAE-SPLADE, a sparse retrieval framework built on sparse autoencoders (SAE), which is an architecture that learn sparse, interpretable latent representations. By using SAE latents as the retrieval vocabulary, SAE-SPLADE removes the dependence on fixed token vocabularies and improves flexibility and representation capacity. Finally, recognizing the efficiency challenges HotBERT, we propose a theoretically lossless token-pruning method for late interaction models that reduces computation while preserving retrieval performance.

Over the last few years, we have been experimenting with using flavours of (coinductive) monadic interpreters to represent computations in Rocq. The basic toolbox of the approach has been embedded back in 2020 in the Interaction Trees library, and notably used at scale in the Vellvm project to give a formal semantics to LLVM IR. In this talk, I will walk through this experience, with the aim to focus in particular on the comparatively more recent treatment of non-determinism. I will introduce so-called Choice Trees, a second library adding support for a choice operator. On top of this primitive operation, we implement shallow combinators for various flavours of parallel composition, whether w.r.t. to shared memory model or communication-based computations. Furthermore, additionally to the monadic interpretation of operations, choice trees support refinements of its internal branching, allowing for executing the semantics against specific schedulers, whether internally to Rocq or on the OCaml side. Finally, and if time permit, I will move the focus to ongoing work with Peio Borthelle around, for lack of talent in naming, monadic trees. This time, we step back to a mathematically more natural approach, albeit more challenging to implement: rather than implementing effect through monad transformers on top of itrees, we directly construct the final coalgebra of the composition of a monad `m` with a functor of observation. ITrees become the specialised case where "m=id", CTrees are essentially isomorphic to the case of "m=fam", the functor of families, and a more generic theory can be established.

Framing lattices were introduced very recently in [von Bell--Ceballos, 2025] and [Berggren--Serhiyenko, 2024] as a wide family of lattices containing many generalizations of the Tamari lattice and the weak order. They are associated to a directed acyclic graph, together with a framing, a choice of total orders on incoming and outgoing edges at each vertex. Such a choice of framing enables to decide whether two routes (maximal paths) are crossing. Framing lattices were then defined as an order on maximal collections of non crossing routes. In an ongoing work with Jonah Berggren, we introduce cornered cliques as a new combinatorial model for the elements of a framing lattice, with explicit bijections with maximal cliques. These enable us to provide cubical coordinates for all framing lattices, for which covering relations change only one coordinate, and comparison in the lattice corresponds to componentwise comparison. These specialize to the well-known bracket vectors for the Tamari lattice, and to an enhanced version of the Lehmer code for the weak order.

Low-discrepancy sequences are the best discrete approximations of the continuous uniform distribution. Two of the most classical constructions are the van der Corput sequence and the family of Kronecker sequences. Apart from their uniformity, their construction methods lead to very nice mathematical properties. In this talk, I will present some ways to use their regularity, first to tackle an old problem of Erdos and de Bruijn (1949) on lengths of consecutive segments, and then to obtain embeddings in translation surfaces.

La bisimulation est une technique de preuve pour montrer que 2 programmes "font la même chose". Je ferai un panorama rapide des bisimulations pour le lambda-calcul, avant de faire l'état de l'art des bisimulations définies jusqu'ici pour les calculs "linéaires" et voir quelles questions restent pour l'instant non résolues.

This talk presents research contributions on Boolean Satisfiability (SAT) solving and its application to the analysis of discrete systems. The first part focuses on parallel SAT solving, addressing key issues such as modular solver design, the articulation between divide-and-conquer and portfolio approaches, and effective learned-clause sharing. In this context, the PaInleSS framework is introduced as a generic platform for building efficient parallel SAT solvers. The second part considers domain-aware SAT solving through programmatic extensions of CDCL, showing how problem-specific knowledge can improve solving strategies, especially in bounded model checking. The presentation concludes with an application to the verification of blockchain smart contracts, where SAT-based reasoning provides a promising basis for analyzing security- and safety-critical properties at scale.

Ce séminaire présente des travaux portant sur le développement d’approches formelles centralisées, modulaires et distribuées pour la modélisation, le contrôle, l’analyse des performances, la reconfiguration et la cybersécurité des systèmes à événements discrets. Ces travaux s’appuient sur différents formalismes tels que les réseaux de Petri (temporisés et colorés), les automates temporisés avec gardes, les automates hybrides, ainsi que les algèbres Max-Plus et Min-Plus et les séries formelles colorées. L’objectif est de proposer des méthodes d’analyse et d’aide à la décision permettant de garantir certaines propriétés des systèmes, notamment en termes de performance, de sûreté et de résilience. Une attention particulière est portée aux problématiques de modélisation et de vérification analytique dans des architectures d’automatisation distribuées (collaboration avec EDF). Les techniques formelles établies sont illustrées à travers plusieurs domaines d’application, notamment la résilience des chaînes logistiques, l’analyse du temps de réponse des systèmes de commande en réseau, les systèmes manufacturiers soumis à contraintes et la sécurité des systèmes cyber-physiques.

Les applications IoT déployées dans le continuum IoT–Fog–Cloud doivent concilier des contraintes de ressources, qualité de service (QoS), hétérogénéité et dynamique d’exécution, tout en restant robustes face aux pannes. Dans ce contexte, la fiabilité ne peut pas reposer uniquement sur des tests ad hoc : elle doit être construite et argumentée de manière systématique, depuis les exigences jusqu’au comportement observé en exécution. Nous présentons d’abord une approche centrée sur la vérification de mécanismes de tolérance aux pannes dans l’IoT multi-couches. La modélisation en Event-B, via raffinement et invariants, permet de formaliser des stratégies telles que la dégradation contrôlée, le basculement vers des composants de secours et la reprise/retour à un état sûr, tout en générant des obligations de preuve garantissant que ces mécanismes préservent les propriétés de sûreté attendues. Cette étape pose un socle : la résilience doit être spécifiée et justifiée rigoureusement, couche par couche, dans des architectures distribuées. Nous passons ensuite au Fog, où l’enjeu devient la composition de services sous contraintes, depuis les exigences jusqu’au déploiement (et, le cas échéant, l’interaction avec des services cloud). La démarche se décline en étapes : (i) capturer et structurer les exigences (fonctionnelles, coordination, ressources, QoS), (ii) décider un placement correct des composants, (iii) établir une configuration/reconfiguration d’un service composite en arbitrant entre efficacité QoS et fiabilité (notamment transactionnelle), puis (iv) vérifier formellement la cohérence de la composition et des interactions par Event-B. Dans cette dynamique, une perspective consiste à mobiliser des agents conversationnels (systèmes multi-agents conversationnels) pour soutenir l’orchestration et la reconfiguration (négociation de contraintes, adaptation, selection, assistance à la décision), tout en conservant un noyau formel vérifiable. Enfin, nous motivons une évolution méthodologique : Event-B est très puissant pour prouver des invariants et structurer la correction, mais il n’est pas toujours le plus adapté pour explorer exhaustivement certains comportements dynamiques typiques des systèmes distribués (interleavings concurrents, scénarios d’exécution, blocages, vivacité, effets de reconfiguration). Pour couvrir ces aspects, nous proposons de compléter la preuve par du model checking, en introduisant une transformation Event-B ? Réseaux de Petri Colorés (CPN). Cette transformation vise à obtenir un modèle exécutable et analysable, permettant ensuite d’appliquer des techniques de vérification automatique (exploration d’espace d’états, détection de deadlocks, propriétés de vivacité/atteignabilité) et de refermer la boucle : les contre-exemples et scénarios trouvés alimentent l’amélioration du modèle Event-B, des exigences et des politiques de configuration. Mots-clés Continuum IoT–Fog–Cloud, Fiabilité / Résilience, Qualité de service (QoS), Tolérance aux pannes multi-couches, Composition et (re)configuration de services, Placement sous contraintes, Vérification formelle, Event-B, Réseaux de Petri colorés (CPN), Model checking, systèmes multi-agents conversationnels

Rational synthesis studies the automatic construction of controllers that interact with rational agents pursuing their own objectives. Rather than assuming a hostile environment, this framework accounts for strategic behavior and equilibrium reasoning in multi-agent systems. In this talk, we consider rational synthesis in the presence of shared resources. Agents interact in turn-based games where actions may consume or replenish common resources, and must satisfy qualitative temporal objectives while avoiding resource depletion. We discuss how resource constraints fundamentally impact the synthesis problem, how the model evolves from single to multiple resources, and what this reveals about the limits of automated controller design.

On peut facilement plier une feuille de papier rectangulaire, afin de réaliser un cylindre droit : il suffit de plier la feuille en trois de manière à obtenir un prisme à section triangulaire. Mais qu'en est-il si l'on veut recoller les bords triangulaires de ce prisme pour réaliser un tore plat ? Nous verrons dans cet exposé que cela est toujours possible, ce quel que soit les polygones papiers de départ considérés, et les instructions de recollement choisis. Nous étudierons également la question suivante : est-il possible de réaliser tous les tores plats avec une combinatoire fixée ? Enfin, si le temps le permet, nous évoquerons la généralisation de ces questions à des surfaces polyédrales de genre 2, dites de translation.

This talk is organized into three main parts. The first part introduces research on Petri net structure theory and robust/adaptive supervisory control of discrete event systems, including controllability of siphons, supervisory control based on time constraints, and robust/adaptive supervisory control for systems with uncertainties caused by unreliable resources or operations. The second part concerns security analysis and resilient control of cyber-physical systems (CPSs) under information impairment. It discusses opacity analysis and resilient supervisory control strategies in the presence of cyberattacks and malicious intrusions. Furthermore, the talk addresses fault diagnosis in CPSs with communication delays. Finally, the talk highlights several future research directions, including prognosability analysis in CPSs with communication delays and the integration of data-driven approaches with supervisory control theory, aiming to enhance the security and resilience of next-generation CPSs.

The Quantum Approximate Optimization Algorithm (QAOA) has recently been proposed as a heuristic framework for solving combinatorial optimization problems through a hybrid classical–quantum optimization procedure. The algorithm alternates parameterized quantum transformations with a classical optimization step that adjusts the circuit parameters in order to increase the probability of sampling high-quality solutions. A key factor influencing the performance of QAOA is the choice of the initial state. In standard implementations, the algorithm starts from a uniform superposition over all candidate solutions, which does not exploit structural information about the original optimization problem and may lead to inefficient parameter optimization and lower-quality solutions. In this talk, we propose a warm-start strategy based on continuous optimization, using the Difference-of-Convex Algorithm (DCA). The idea is to exploit a continuous relaxation of the original optimization problem in order to construct an informed initialization that biases the search toward promising regions of the solution space. We illustrate the approach on instances of the Max-Cut problem and show that this strategy can significantly improve the approximation ratios obtained by QAOA. This is a joint work with HA Huy Phuc Nguyen et TA Anh Son.

Positive spanning sets (PSSs), that span a given space through nonnegative linear combinations, have been successfully employed to design and analyze derivative-free optimization algorithms. Although linear algebra is a natural framework for studying PSSs, polyhedral geometry can provide additional insights on the structure of PSSs. In this talk, I will first introduce the concept of positive spanning sets, together with its use in derivative-free optimization. I will then focus on the specific case of polyhedral constrained problems, and explain how to generate positive spanning sets that conform to the geometry of those constraints. Finally, I will turn to a perhaps unexpected construction of PSSs of smallest cardinality through polytopes, and discuss several associated open questions. This talk is based on joint works with Denis Cornaz, Sébastien Kerleau and Lindon Roberts.

Cette présentation plonge, en particulier, dans l'article https://arxiv.org/abs/2510.03177 avec Georg Loho et Arnau Padrol. Nous commencerons par une (longue) introduction aux déformations de polytopes. Un permutoèdre déformé (aussi appelé permutoèdre généralisé, ou fonction sous-modulaire) est un polytope dont toutes les arêtes ont pour direction $e_i - e_j$ pour certains $i \neq j$. L'ensemble des permutoèdres déformés vivant dans $\mathbb R^n$ forme un cône, le cône sous-modulaire. Nous proposons une construction "inductive" du cône sous-modulaire, en utilisant une opération nommée GP-sum : à partir de deux permutoèdres déformés dans $\mathbb R^n$, nous créons (bijectivement) un permutoèdre déformé dans $\mathbb R^{n+1}$. Munis de cette construction, nous créons de nouveaux rayons du cône sous-modulaire, c'est-à-dire de nouveaux permutoèdres déformés indécomposables (au sens de la somme de Minkowski). Cela nous permet d'améliorer les bornes connues sur le nombre de rayons du cône sous-modulaire, notamment en produisant $2^{2^n}$ rayons. Plus encore, nous étudions le f-vecteur du cône sous-modulaire, son nombre total de faces, et le nombre de ses faces simplicial, grâce à la nouvelle partition que cette construction inductive nous donne.

While the ?-calculus is widely recognized as a model of computation, equivalent to Turing and other machines, its relevance for the study of complexity has long been unclear. Its central operation, ?-reduction, seems at first sight too rich and complex to be considered as an appropriate atomic unit of computation. We learned only quite recently that the natural complexity measures (number of ?-reductions for time, size of terms for space) were indeed ''reasonable'' measures, defining the same complexity classes (P, NP, PSPACE, ...) as the Turing standard. In this talk I will propose a refined —but still simple and natural— definition of space complexity for the ?-calculus, sensitive to sub-linear space. In particular, this measure allows a ?-calculus-based characterization of algorithms running in logarithmic space (class L), thus extending the range of complexity classes for which the ?-calculus is an appropriate vessel.

Même si trier une permutation aléatoire requiert n log(n) comparaisons en moyenne, il existe de nombreux cas d'usage où les tableaux que l'on souhaite trier ne sont pas des permutations aléatoires : soit ils contiennent de longues plages contiguës déjà triées, soit ils contiennent peu de valeurs distinctes. L'algorithme TimSort, utilisé en Java pour trier des tableaux d'objets composites, a été conçu spécifiquement pour être plus efficace sur de tels tableaux pré-triés. Nous découvrirons comment cet algorithme et ses variantes fonctionnent et pourquoi ils sont efficaces.

As originally showed by Barr, a topology on a set X can be equivalently described as a 'convergence relation' between elements of X and ultrafilters on X: in other words, a spatial locale can be recovered from its set of points once it is endowed with appropriate extra structure defined in terms of ultrafilters. In this talk, I will present a similar reconstruction result for (Grothendieck) toposes with enough points, a categorification of spatial locales: every such topos can be recovered up to equivalence from its category of points, provided that the latter is endowed with appropriate extra structure involving ultrafilters. In logical terms, this reads as a (strong) conceptual completeness theorem for geometric logic. Towards this goal, I will introduce ultraconvergence spaces, a profunctorial generalization of Makkai's ultracategories inspired by Barr's convergence relations. This talk is based on joint work with Quentin Aristote, Sam van Gool and Jérémie Marquès.

Given an hypergraph on a set of n ordered vertices, we define an independent set X to be feasible, if X is a possible outcome for a player in a sequential picking game, against a greedy adversary, where no hyperedge can be contained in the union of both outcomes. We prove that testing feasibility is NP-complete, even if the hypergraph is a graph, but it becomes polynomial (in n) for matroid hypergraphs, that is, when the hyperedges are the circuits of some matroid (in which independence can be tested with an oracle). We prove also that optimizing a linear function over feasible sets is NP-hard for graphs and matroid hypergraphs, even for graphic matroids, but it becomes polynomial for laminar matroids.

Geometric hitting set problems, in which we seek a smallest set of points that collectively hit a given set of ranges, are ubiquitous in computational geometry. Most often, the set is discrete and is given explicitly. We propose new variants of these problems, dealing with continuous families of convex polyhedra, and show that they capture decision versions of the two-level finite adaptability problem in robust optimization. We show that these problems can be solved in strongly polynomial time when the size of the hitting/covering set and the dimension of the polyhedra and the parameter space are constant. We also show that the hitting set problem can be solved in strongly quadratic time for one-parameter families of convex polyhedra in constant dimension. This leads to new tractability results for finite adaptability that are the first ones with so-called left-hand-side uncertainty, where the underlying problem is non-linear. Joint work with Jean Cardinal and Xavier Goaoc. Manuscript: https://arxiv.org/abs/2504.16642

Betweenness centrality (BC), introduced in 1977, is a fundamental measure of node importance in networks, widely used in fields ranging from sociology to computer science. BC quantifies the extent to which a node lies on shortest paths between pairs of nodes, making its computation closely tied to the enumeration of these paths. In this work, we investigate the computational complexity of determining BC for all nodes in a graph, highlighting the challenges associated with exhaustive shortest-path counting. We further examine extensions of BC to dynamic graphs, where edges carry temporal information and optimal paths are determined not only by topology but also by timing constraints (i.e., fastest paths). We explore the hardness of computing BC under such dynamic conditions and discuss how temporal dependencies complicate classical shortest-path approaches. Our study aims to unify understanding of BC computation across static and temporal graph models and to identify open problems in efficiently counting relevant paths in these settings.

This presentation addresses linear Chance-Constrained Stochastic Problems (CCSPs) with finite support. We begin by motivating the study of CCSPs through illustrative examples and providing intuition regarding the concept of feasibility in this context. Subsequently, we discuss the computational challenges inherent to these problems, specifically the nonconvex structure of the feasible region and the limitations of the standard big-M reformulation. These challenges necessitate the use of branch-and-cut approaches. To this end, we review existing families of valid inequalities, such as quantile inequalities and mixing inequalities. This background sets the stage for the primary contribution of this work: a new class of valid inequalities termed multi-disjunctive inequalities. We construct these inequalities by exploiting a disjunctive property inherent to the mathematical formulation of CCSPs. Theoretical analysis reveals that the closure of these multi-disjunctive inequalities constitutes a proper subset of the closure generated by previously proposed families. We perform numerical experiments within a pure cutting-plane framework to compare the closures obtained by enumerating all violated valid inequalities. The results demonstrate that multi-disjunctive inequalities significantly strengthen the continuous relaxation of the considered CCSPs compared to existing quantile and mixing-set inequalities. Furthermore, we evaluate the performance of these inequalities embedded within a branch-and-cut framework. Our results indicate that the proposed approach significantly outperforms existing methods on both standard literature instances and newly generated instances designed to be computationally challenging.

Étant donné $n \in \mathbb{N}$ et $\mu \in \mathbb{R}$, un arbre de taille $n$ biaisé par la hauteur est un arbre planaire aléatoire $T_n$ à $n$ sommets dont la loi est donnée par $P(T_n = t ) \propto e^{-\mu h(t)}$, où $t$ est un arbre fixe à $n$ sommets, et $h(t)$ est la hauteur de $t$ . Dans cet exposé on va présenter quelques statistiques de ces arbres quand $\mu=\mu(n)$ est une suite à termes positifs dépendant de $n$: la limite d'échelle quand $\mu(n) \sim 1/ \sqrt{n}$, la hauteur ainsi que le comportement autour de la racine quand $0 \leq \mu(n) \ll n$. L'exposé est basé sur arXiv:2512.17747 en commun avec L. Addario-Berry, B. Corsini et N. Maitra.

A fundamental operation in type systems is the ability to *type cast*, that is, take a value of a given type and use it at different type, assuming some information relating the source and target. This manifests under many names: subtyping, coercion, transport... These various mechanisms are particularly essential in dependent type theory, where types are extremely rich and precise. Yet they have a complicated history, and are rather poorly understood from a theoretical standpoint. In my talk I will explain the challenges faced with cast systems, and how we can understand and fix some of them with the type theorist's glasses on. The focus will be particularly on *structural* casts, those that follow the structure of type formers, which led us to a surprisingly deep and beautiful type theoretic quest, revolving around the idea that structural casts arise from the fact that all type formers are really functors.

Lattice walks confined in the first quadrant have been subject to an extended study for about a decade, showing a great variety of techniques to handle functional equations with catalytic variables. A work of Pierre Bonnet and Charlotte Hardouin of 2024 extended those tools in the context of the study of walks based upon models with arbitrarily large steps, allowing to effectively conduct a strategy devised by Bousquet-Mélou, Olivier Bernardi and Kilian Raschel of 2016, providing the algebraicity proofs of some models. In this talk, I show how these tools show the algebraicity of an infinite family of models of walks derived from the Gessel models.

Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abstraction functions to demonstrate the coherence between such concrete implementations and their abstract specifications. However, the Hoare methodology relies on a conventional separation between implementation and specification, providing no linguistic support for ensuring that this convention is obeyed. The presented work proposes a synthetic account of Hoare's methodology within univalent dependent type theory by encoding the data of abstraction functions within types themselves. This is achieved via a phase distinction, which gives rise to a gluing construction that renders an abstraction function as a type and a pair of modalities that fracture a type into its concrete and abstract parts. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory. This approach scales to verification of cost, allowing the analysis of client cost relative to a cost-aware specification. A monadic sealing effect facilitates modularity of cost, permitting an implementation to be upper-bounded by its specification in cases where private details influence observable cost. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.