2 December 2024 at 13:00 in Room 301 (Battelle A)

18 November 2024 at 12:30 in Room 301 (Battelle A)

In this talk, I will first present the standard attention-based operations that have been so successful for large language models, and will show how we have used these techniques to devise state-of-the-art world models for reinforcement learning. The I will expose preliminary results for the self-generation of non-NLP reasoning tasks that expend a basic set of simple hand-designed reasoning challenges. This approach provides a blueprint of a possible strategy to develop abstract reasoning beyond reinforcement learning, without using human-generated data.

11 November 2024 at 12:30 in Room 301 (Battelle A)

Locally checkable problems are vertex partitioning problems for which a solution has to satisfy some local property for each vertex (that is, a property that involves only the solution restricted to the vertex and its neighbors). This is the case of several variants of minimum dominating set, maximum independent set and k-coloring, among others. In this talk, we will delve into the question of what makes locally checkable problems easy or hard, when restricted to certain graph classes. Specifically, we will study the conditions that locally checkable problems must satisfy in order to be XP parameterized by mim-width.
Link to the paper
Link to the presentation

4 November 2024 at 12:30 in Room 301 (Battelle A)

Mobile crowdsensing (MCS) is a recent paradigm, which leverages the sensing data from the mobile devices of people (the crowd) to serve various goals. These include business goals as for example designing and evaluating a health care product by using the cumulative data gathered by a crowd through the powerful sensors integrated in smartphones. Moreover, MCS is used to improve public and individual services. In this talk, I present a selfish atomic routing game that serves as model to optimize the allocation of tasks in a MCS system. For the Nash equilibria of our game, we can transfer efficiency guarantees, i.e., the worst-case ratio between the welfare of an equilibrium and the welfare of a social optimum is provably bounded by a small constant when cost functions are polynomials. An epsilon-approximation of a Nash equilibrium solution can be computed in polynomial time for affine cost functions. Based on the analysis using our model, we derive a mechanism for the automation of efficient task allocations in MCS and we prove that the mechanism is truthful. At the end of the talk, I briefly present initial results from an ongoing project in cooperation with the Swiss Tropical and Public Health Institute in Basel and the Citizen Science Center of ETH Zurich to monitor electromagnetic radiation using MCS.

14 October 2024

A temporal graph is a graph whose edges are only present at certain points in time. These graphs received a growing attention over the past two decades, due to their ability to model various types of dynamic networks. On the theoretical side, temporal graphs are quite different from static graphs. For instance, reachability (defined in terms of paths that traverses edges in chronological order) is not transitive. This and other features have important consequences, both structural and algorithmic, most questions becoming computationally hard. In this talk, I will review some basic results in this young field, with a focus on reachability questions.

29 February 2024

Deductive verification provides very strong guarantees that software is bug-free. Since the verification is usually done at the source level, the compiler becomes a weak link in the software-production chain. Verifying the compiler itself provides guarantees that no errors are introduced during compilation. This talk will illustrate this approach through CompCert, the first fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.

18 January 2024

Dans cet exposé qui se veut introductif, je commencerai par décrire les principes qui régissent la sémantique des jeux de la logique linéaire. Dans cette interprétation interactive de la logique, toute formule A définit un jeu de dialogue à deux joueurs dans lequel le joueur cherche à établir la validité de la formule A tandis que l’opposant cherche à la refuter. Une démonstration de la formule A est interprétée par une stratégie gagnante du jeu de dialogue associée, qui assure au joueur qu’il convaincra l’opposant et gagnera la partie. J’expliquerai comment la notion de jeu de gabarit (template game) que j’ai introduite il y a quelques années permet d’adapter ces idées à la programmation impérative et concurrente avec mémoire partagée, pour établir la correction de la logique de séparation concurrente.

11 January 2024

PADEC is a framework to build machine-checked proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, tools for time complexity and composition of algorithms, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions. In this talk, we focus on the composition of algorithms: the correctness proof contains a lazy-productive operator called ‘squeeze’. This operator transforms a stream in order to remove repeats under some decidable conditions.

19 December 2023

We study the kernelization of exploration problems on temporal graphs. A temporal graph consists of a finite sequence of snapshot graphs G = (G1, G2, …, GL) that share a common vertex set but might have different edge sets. The non-strict temporal exploration problem (NS-TEXP for short) introduced by Erlebach and Spooner, asks if a single agent can visit all vertices of a given temporal graph where the edges traversed by the agent are present in non-strict monotonous time steps, i.e., the agent can move along the edges of a snapshot graph with infinite speed. The exploration must at the latest be completed in the last snapshot graph. The optimization variant of this problem is the k-arb NS-TEXP problem, where the agent’s task is to visit at least k vertices of the temporal graph. We show that under standard computational complexity assumptions, neither of the problems NS-TEXP nor k-arb NS-TEXP allow for polynomial kernels in the standard parameters: number of vertices n, lifetime L, number of vertices to visit k, and maximal number of connected components per time step γ; as well as in the combined parameters L + k, L + γ, and k + γ. On the way to establishing these lower bounds, we answer a couple of questions left open by Erlebach and Spooner. We also initiate the study of structural kernelization by identifying a new parameter of a temporal graph Informally, this parameter measures how dynamic thetemporal graph is. Our main algorithmic result is the construction of a polynomial (in p(G)) kernel for the more general Weighted k-arb NS-TEXP problem, where weights are assigned to the vertices and the task is to find a temporal walk of weight at least k.

23 November 2023

After a brief overview of my journey from automated deduction, its formal certification, and towards verification of distributed protocols, I will present our work in the context of autonomous mobile robots in swarms. In this recent model, robots compute their actions based on their own perception of their surroundings. Characterized by extreme dynamicity and versatility, these swarms allow to envision numerous applications: exploration of dangerous/devastated areas, search and rescue, setting up of dynamic networks, etc. Their formal verification, compulsory in the case of critical/life and death scenarii, brings formidable challenges to tackle. To this goal, we develop Pactole, a formal framework mechanised for the Coq proof assistant. As Pactole allows for establishing correctness of distributed protocols for robotic swarms; it also proves useful to show formally that some tasks are indeed unfeasable under particular assumptions.