We organize weekly/biweekly meetings in our group with invited speakers, but also with presentations by members of our group. Stay tuned!
Upcoming seminars
28 October 2024 at 12:30 in Room 301 (Battelle A)
Julia Buwaya (University of Geneva)
Mobile crowdsensing through the lens of algorithmic game theory
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.
4 November 2024 at 12:30 in Room 301 (Battelle A)
Carolina Lucía Gonzales (University of Fribourg)
TBD
Past seminars
14 October 2024
Arnaud Casteigts (University of Geneva)
Temporal graph theory: paradigm and algorithmic challenges
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
Sandrine Blazy (IRISA, University of Rennes)
How to provide proof that software is bug-free? Verified compilation to the rescue
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
Paul-André Melliès (IRIF, CNRS, Paris)
Sémantique des jeux: une interprétation interactive de la logique
linéaire et de la logique de séparation concurrente
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
Karine Altisen (Verimag, University of Grenoble)
Interactive Proof for Self-Stabilizing Algorithms using PADEC: Squeezing Streams
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
Petra Wolf (University of Bordeaux)
Kernelizing Temporal Exploration Problems.
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
Xavier Urbain (LIRIS, Univ. Claude Bernard, Lyon)
Safety and Versatility: verifying swarms of autonomous robots
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.