I am interested in verification of distributed systems with an unbounded number of agents running the same finite-state program. These include systems like conservative Petri nets, population protocols, reconfigurable broadcast networks and more. Properties of interest for these systems are “parameterized”: for example, is there a number of agents N such that my system instantiated with N agents reaches a bad configuration? I will present a recent result on HyperLTL for population protocols, where we will see that the verification problem can be cast as a parameterized reachability property. I will then present some open questions for parameterized verification of such systems. If I have time, I will present my newest research direction which concerns runtime verification of distributed systems, and the hypotheses that can be made on the setting.

Beginning in the 1950’s, with an eye to the (then) four-colour conjecture, Tutte defined the notion of nowhere-zero (nz) flow on a graph, and stated three famous flow conjectures: 5-flow, 4-flow, and 3-flow. This notion was generalized to nz flows on signed graph by Bouchet in 1983, and he made a 6-flow conjecture analogous to Tutte's 5-flow conjecture. Recently, I have shown that Bouchet's conjecture holds for cyclically 5-edge-connected cubic graphs. The proof of this result uses edge-contractions to reduce the size of the graph in question, which I believe is a powerful and somewhat overlooked tool.

While it is fascinating to explore what quantum computers are capable of, it is equally important to study their limitations. One way to do this is by proving explicit lower bounds on the quantum query complexity of computational problems.

One of the frameworks to prove these lower bounds is the compressed oracle technique [Zha19], which can be used to derive quantum query lower bounds for problems where a quantum algorithm interacts with a quantum oracle that accesses a random function. This framework has proven to be very useful and convenient to use, since deriving a lower bound reduces to mostly combinatorial arguments. It is unclear, however, how this frameworks compares with the more established lower bound methods for quantum query complexity.

In this talk, we show how the compressed oracle technique can be reduced to the multiplicative adversary method [Spa08] and discuss how this could give insights into generalising the compressed oracle technique to go beyond random functions.

Based on joint work with Stacey Jeffery

An important question in the domain of distributed computing is that of task solvability : given a distributed task, the analog of a program specification for distributed systems, under which conditions can it be solved by some distributed protocol ? The topological approach to distributed computing represents tasks and protocols as relations between simplicial complexes, combinatorial objects which encode possible global states of the system. These have a spatial interpretation, which led to the Asynchronous Computability Theorem (ACT), which relates, for certain computational models, the existence of a continuous map to task solvability, using subdivisions of the input space.

In this talk, I will present a generalisation of the ACT for colourless protocols based on categorical and duality theoretic constructions. This is achieved by viewing an iterated protocol as an endofunctor on the category of simplicial complexes, along with a natural transformation encoding the relation between inputs and computational outputs. From this data we produce, for each possible set of inputs, a limit object in the form of a spectral space which encodes all possible computational outputs, and characterises the task solvability of the protocol. Indeed, a protocol can solve a task if, and only if, there exists a continuous map from the associated spectral space to the space of outputs. This construction works for any iterated protocol, but we additionally show that it is compatible with the original approach using subdivision protocols, since in this case, the geometric realisation, the space used in the original ACT, is a canonical subspace of the associated spectral space.

See https://chocola.ens-lyon.fr/events/seminaire-2025-12-11/

Consider a data structure problem with possible data coming from a set D, queries coming from a set Q, and in the dynamic case updates coming from a set U. Then, the current state of the art in data structure lower bounds is t = \tilde\Omega(\log Q|) for static data structure problems, and max(t_q,t_u) = \tilde\Omega(log^2 n) where n = max(|Q|,|U|,log |D|) for dynamic.

We port Razborov and Rudich's natural-proofs framework to the setting of static and dynamic data structures in the cell probe model, in a way that strongly suggests this state of the art is unlikely to be improved anytime soon. A similar direction was recently taken also by Korten, Pitassi and Impagliazzo (FOCS 2025) who look at static data structure lower bounds in a different regime of parameters. Our contribution is:

- We define notions analogous to pseudorandom functions (PRF). We call these primitives *local PRFs*, in the context of static data structures, and *local and locally updatable (LLU) PRFs*, in the context of dynamic data structures.

- We then formulate cryptographic conjectures, namely, that secure local PRFs and secure LLU PRFs exist, precisely at the frontier where we are no longer able to prove static, respectively dynamic, data structure lower bounds. If these conjectures are true, it follows that the current state of the art in data structure lower bounds cannot be improved by a natural proof.

- We show that (almost) every single known data structure lower bound proof is a natural proof, by surveying all lower bounds in the literature (known to us). (The only exception is proofs based on lifting theorems.)

- It follows that, if our cryptographic conjecture is true, then all known lower bound proof techniques (minus the two exceptions) are unable to improve upon the state of the art. (We also present obstacles for the two exceptions.)

- Further, we provide concrete candidate constructions for our two pseudo-random primitives. We conjecture that our constructions are secure for parameters just above the state-of-the-art lower bounds.

- We also show that, whether or not they are secure, our candidate PRFs at least satisfy the natural properties appearing in all (but one) known proofs.

- So if one is interested in improving upon the state of the art in static or dynamic data structure lower bounds, one must either find a non-natural method of proving such lower bounds (no such method currently exists), or one may as well begin by trying to break our PRF candidates.

Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. We introduce a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction.

This work was presented at CONCUR 2025.

Cangjie is a high-level, statically typed, general-purpose, multi-paradigm, compiled imperative and declarative programming language developed by Huawei. It was first released on June 21, 2024, as part of developer beta recruitment, for HarmonyOS NEXT app development on the preview version of the HarmonyOS operating system. It is also referred to as CangjieLang or CJ, but its proper name is Cangjie.

Reference: https://cangjie-lang.cn/en/docs

Consider a simple (to formulate…) mathematical object: you are given a finite collection of matrices $A_i\in GL(2,\mathbb R); i=1,\ldots,k$ and you are allowed to multiply them, in any order. The notion you are interested in is the exponential rate of speed of growth of the norm: given $\omega\in \{1,\ldots,k\}^{\mathbb N}$, let \[ \lambda(\omega) = \lim_{n\to\infty} \frac 1n \log ||A_{\omega_n} \cdot \ldots \cdot A_{\omega_1}||. \] This object has many names, in dynamical systems we call it the Lyapunov exponent.

We are in particular interested in the set of those $\omega$'s that give the extremal (maximal, minimal) value of the Lyapunov exponent. A long-standing conjecture states that for a generic matrix collection those sets ought to be {\it small}, in some sense. In the result I will present we (Jairo Bochi and me) are proving that for certain open set of collections of matrices those $\omega$'s that maximize/minimize Lyapunov exponent have zero topological entropy.