Differential privacy (DP) is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of DP, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We have identified common themes in existing ad hoc definitions and introduced an alternative notion of accuracy parametrized by a reference specification φ. We say that a DP algorithm is (μ, β)−accurate w.r.t to φ iff φ is ’almost true’ with tolerance μ and a high probability 1 − β. We proposed a synthesis method, that takes as an input the program specification φ and produces a probabilistic accuracy statement. Our approach applies to programs that are made DP by introducing a random noise to their input. The approach is systematic and is reduced only on logical reasoning. It uses axiomatic properties of probability distributions combined with FO deductive techniques in order to derive an probabilistic accuracy specification about the DP program from the specification of the original program. In order to make tighter accuracy statements, we proposed an extension to our approach that takes into account assumptions about the input values and reason about accuracy without compromising the privacy.

(Joint work with Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, and Atsushi Igarashi)

A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool HELMHOLTZ for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. HELMHOLTZ is designed on top of our extension of Michelson's type system with refinement types. HELMHOLTZ takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. HELMHOLTZ successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

(Joint work with Sylvie Putot).

In this talk, we will discuss range analyzes for feedforward neural networks, which are basic primitives for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems.

We will describe too current work in progress. The first one focuses on analyzing networks in isolation, and in particular ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. We use here set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We will present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra.

The second one will show how to analyze networks in a closed feedback loop, as e.g. a controller in a Cyber-Physical System (CPS). We will focus here on differentiable activation functions and will show how Taylor models that have been instrumental in the analysis of CPS leverage to the analysis of networks in the loop, even allowing for computing guaranteed (robust) inner and outer-approximations.

Workflow nets are a popular variant of Petri nets that allow for the algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with soundness, where the initial and final configurations are specified. Intuitively, soundness states that from every reachable configuration one can reach the final configuration. In recent work, we settle the widely open complexity of the three main variants of soundness: classical, structural and generalised soundness. The first two are EXPSPACE-complete, and, surprisingly, the latter is PSPACE-complete, thus computationally simpler. In this talk, I will 1) introduce the soundness problem and its variants, and 2) give insights into the complexity results for the three variants, mostly focussing on the upper bounds.

We study the zeroness and equality problems for weighted register automata over equality data. We reduce these problems to the problem of counting the number of orbits of runs of the automaton. We show that the resulting orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind. We then show that zeroness / equality of weighted register automata reduces (in exponential time) to the zeroness problem for linrec sequences.

While such a counting approach is classical and has successfully been applied to weighted finite automata over finite alphabets and weighted grammars over a unary alphabet, its application to register automata over infinite alphabets is novel. We provide an algorithm to decide the zeroness problem for the linrec sequences arising from orbit-counting functions based on skew polynomials and variable elimination. This algorithm has elementary complexity.

The complexity can be improved by computing the Hermite normal form of matrices over a skew polynomial field, which leads to a EXPTIME decision procedure for the zeroness problem of linrec sequences, and a 2-EXPTIME decision procedure for the zeroness / equality problems for weighted register automata over equality data.

These results have appeared in STACS'21 in joint work with Corentin Barloy. It has been shown in LICS'21 by Bojańczyk, Klin, and Moerman that the complexity of zeroness / equality of weighted register automata can be improved to EXPTIME, using novel techniques involving a deep study of orbit-finite vector spaces.

Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was recently studied in [Geeraerts et al 2011,2014], where the authors also proposed a solution using extrapolations.

In our work, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the G-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.

Linear recurrence sequences (LRS) are infinite sequences of integers whose nth entry is a linear combination of the previous d entries, for a fixed d. The set of indices that correspond to the positive entries of such a sequence is called its positivity set. Given a LRS, deciding whether its positivity set is empty or not is a long standing open problem. Its solution would imply decidability of the halting problem for linear loops, it would allow us to effectively solve a family of exponential diophantine equations (Skolem problem), and it would give a profound understanding of some aspects of transcendental numbers; to name just a few corollaries.

In this talk I will discuss a statistical facet of the positivity set, namely its density as a subset of positive integers. I will show that this quantity is equal to the volume of a certain constructible subset of euclidian space, and how to approximate said volume using a result of Koiran. Time permitting, I will tell you how in pursuit of a procedure to decide whether the density is larger than some given rational number, one is led to questions about the algebraic relations among periods, and how in certain cases the difficulties are overcome with Chebyshev polynomials.

Computing a mission plan for an autonomous vehicle consists of path planning and task scheduling, which are two outstanding problems existing in the design of multiple autonomous vehicles. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space-explosion problem that makes it inefficient at solving the problem when the number of vehicles is large, which is often the case in realistic scenarios. In this talk, we show how reinforcement learning can help model checking to overcome these limitations, such that mission plans can be synthesized for a larger number of vehicles if compared to what is feasibly handled by model checking alone. Instead of exhaustively exploring the state space, the reinforcement-learning-based method randomly samples the state space within a time frame and then uses these samples to train the vehicle models so that their behavior satisfies the requirements of tasks. Since every state of the model needs not be traversed, state-space explosion is avoided. Additionally, the method also guarantees the correctness of the synthesis results. The method is implemented in UPPAAL STRATEGO and integrated with a toolset to facilitate path planning and task scheduling in industrial use cases. We also discuss the strengths and weaknesses of using reinforcement learning for synthesizing strategies of autonomous vehicles.

Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and associated lemmas, which constitute an integral part of proof construction. Following this – whether automatic or semi-automatic – methods for computer-aided lemma discovery have emerged. In this work, we introduce a new symbolic technique for bottom-up lemma discovery, that is, the generation of a library of lemmas from a base set of inductive data types and recursive definitions. This is known as the theory exploration problem, and so far, solutions have been proposed based either on counter-example generation or the more prevalent random testing combined with first-order solvers. Our new approach, being purely deductive, eliminates the need for random testing as a filtering phase and for SMT solvers. Therefore it is amenable compositional reasoning and for the treatment of user-defined higher-order functions. Our implementation, TheSy, has shown to find more lemmas than prior art, while avoiding redundancy and without having to run the programs once.

In this talk, I will present results published in CAV 2021, and ongoing work on extending TheSy to richer theories. In the first work, we used e-graphs on top of egg (Willsey et al). In the follow-up, we extend egg to be able to handle conditional equalities, which are pervasive in many theories; notably, Separation Logic with inductive definitions. We hope that this will allow synthesizing a richer set of lemmas.

I will introduce a multicore algorithm for the parallel detection of Strongly Connected Components. The algorithm uses a concurrent Union-Find forest to share partial SCCs. As a consequence, we get parallel speedup even if the graph consists of a single SCC. The algorithm works on-the-fly, so it is useful for parallel LTL model checking.

Since parallel graph algorithms are error prone, and this one is used in verification tools, we would like to verify it. We will report a first step, modeling the algorithm in TLA+ and model checking it for instances with a few workers and small graphs.

We define timed/register synthesis games as a generalisation of the classical Büchi-Landweber games.

For such games, the problem of synthesising a winning controller turns out to be decidable when we bound the number of clocks/registers the Controller player has at his disposal, and undecidable otherwise.

I will prove the decidability result mentioned above in the setting of register automata, which is a generalisation of the Büchi-Landweber theorem. Additionally, I will mention adaptations needed to move to the timed setting.

Time permitting, I will mention an application of these games to a problem of deterministic separability of NTA/NRA.

We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

In this talk, I will discuss learning algorithms for weighted automata over principal ideal domains (PIDs). I start with discussing properties of the Hankel matrix of a weighted automaton. Then I reiterate briefly the idea behind learning weighted automata over fields. For automata over PIDs, I recall an existing algorithm (Heerdt et al., FoSSaCS 2020) for exact learning that has no complexity bounds (but only termination). I will recall a classical result of Fatou, and, inspired by its proof, draft a simpler learning algorithm for learning weighted automata over PIDs.

Zero-sum stochastic games, henceforth stochastic games, are a classical model in game theory in which two opponents interact and the environment changes in response to the players’ behavior. The central solution concepts for these games are the discounted values and the value, which represent what playing the game is worth to the players for different levels of impatience. In the present manuscript, we provide algorithms for computing exact expressions for the discounted values and for the value, which are polynomial in the number of pure stationary strategies of the players. This result considerably improves all the existing algorithms.

We investigate the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle_{n = 0}^\infty$ of rational numbers and a target $t \in \mathbb{Q}$, decide whether $t$ occurs in the sequence. We show decidability of this problem under the assumption that in the defining recurrence $p(n) u_{n+1} = q(n) u_{n}$, the roots of the polynomials $p(x)$ and $q(x)$ are all rational numbers. Our proof relies on bounds on the density of primes in arithmetic progressions. We also observe a relationship between the decidability of the Membership problem (and variants) and the Rohrlich-Lang conjecture in transcendence theory.

This work is in collaboration with Amaury Pouly, Mahsa Shirmohammadi and James Worrell. The full version of the paper is available at https://arxiv.org/abs/2202.07416 <https://arxiv.org/abs/2202.07416>.

The Skolem Problem asks to decide whether a linearly recurrent sequence (LRS) over the rationals has a zero term. This problem — whose decidability has been open for many decades — has been considered in many contexts, including weighted automata, Markov chains, and linear loops. In this talk we describe a landscape of decision problems on LRS in and around the Skolem Problem, focussing on a recent proof of decidability of the latter for the class of simple LRS and subject to two number-theoretic conjectures: the p-adic Schanuel conjecture and the exponential-local-global principle.

The talk is based on joint work with Y. Bilu, F. Luca, J. Ouaknine, D. Pursar, and J. Nieuwveld.

This is a talk on an ongoing, non-finished, unpublished research.

We study the evolution of “size” of a given timed language with respect to time. Intuitively, we determine, how many bits/second contains a typical word in the timed language.

In previous work we studied the evolution of size with respect to the number of events (that is in bits per event, which could be less relevant). For a given regular timed language, we took all the words having n events, and summed up the volumes of all their timings (as polytopes in R^n).

For languages characterized by a time bound instead of a number of events, unfortunately, this approach is not appropriate anymore. Indeed the polytopes can have different dimensions, even for the same duration. So instead we adopt a point of view inspired by information theory, with two “sizes” closely related to each other. For a timed language L: - the maximal number of different words in L of duration ≤ T that can be distinguished by a “myopic” observer; - the minimal size of a finite set of words sufficient to approximate any word in L of duration ≤ T.

The two measures correspond respectively to the notions of optimal ε-separated subsets and ε-nets, instantiated for a pseudo-distance we introduced in a previous work. This distance characterizes the “myopic” observer, parametrized by its precision of observation ε. The logarithms of these two quantities (i.e. the two measures in bits) are respectively called ε-capacity and ε- entropy.

In this work we are particularly interested in the asympotics of these two measures: hence we define (resp.) capacitive and entropic ε-bandwidth as the limits, as time grows to infinity, of these quantities divided by time.

Our main result is (or will be) the partition of timed automata into 3 classes according to structural criteria, which happen to have bandwidths with 3 distinct asymptotic types with respect to 1/ε: no dependency, logarithmic dependency, or linear dependency.

This is a joint work with Eugene Asarin and Catalin Dima.

In grammar-based compression a string is represented by a context-free grammar, also called a straight-line program (SLP), that generates only that string. The hierarchical structure of SLPs makes them amenable to algorithms that work directly on the compressed representation, without decompressing the string first. I will present a recent balancing result stating that one can transform an SLP of size g in linear time into an equivalent SLP of size O(g) and height O(log N) where N is the length of the represented string. The question whether such a depth reduction was possible while keeping the size linear has been a long-standing open problem in the area of grammar-based compression. Its solution enables a wide range of algorithmic applications on SLPs, with either significantly simplified proofs or improved space/time bounds.

This is joint work with Artur Jeż and Markus Lohrey.

Given as input a finite set of square matrices A_1, …, A_k, the Identity Problem asks to decide whether the identity matrix lies in the semigroup generated by A_1, …, A_k. We show that the Identity Problem is decidable for matrices in UT(4, Z), the group of unitriangular integer matrices of dimension four. This extends the previous decidability result of the Identity Problem for matrices in UT(3, Z), also known as the Heisenberg group. Our main arguments rely on the metabelian property of UT(4, Z). Indeed, the commutator subgroup of UT(4, Z) is isomorphic to Z^3. We will use some tools from convex geometry and algebraic geometry, allowing us to view UT(4, Z) as a geometric object, thus giving intuition on how the identity element may be reached as a semigroup element. If time allows, we will also discuss how similar arguments may be used to tackle the Identity Problem for other unitriangular matrix groups, notably the direct product UT(3, Z)^n, as well as how to potentially extend these arguments to UT(n, Z) for n > 4, where the group ceases to be metabelian.

Traditionally, most verification efforts have focused on the satisfaction of trace properties, such as that an assertion is satisfied at a particular program location or that the computation terminates eventually. Many policies from information-flow security, like observational determinism or noninterference, and many other system properties including promptness and knowledge can, however, not be expressed as trace properties, because these properties are hyperproperties, i.e., they relate multiple execution traces.

In this talk, I will give an overview on recent efforts to develop specification logics and model checking algorithms for hyperproperties. The two principal ideas are the addition of variables for traces and paths in temporal logics, like LTL and CTL*, and the introduction of the equal-level predicate in first-order and second-order logics, like monadic first-order logic of order and MSO. Both extensions have a profound impact on the expressiveness of the logics, resulting in a hierarchy of hyperlogics that differs significantly from the classical hierarchy. Model checking remains decidable for a large part of the new hierarchy. Satisfiability is in general undecidable for most hyperlogics, but there are useful decidable fragments. I will report on first successes in translating these encouraging theoretical results into practical verification tools.

This presentation will focus on a software chain called Hippo that aims to provide tools to design, verify and generate code for embedded real-time applications to ensure their temporal behavior. It is based on the Tina toolkit and an extension of the Fiacre pivot language. The main problem addressed by Hippo concerns the generation of an executable that guarantees the respect of temporal constraints. One difficulty is to avoid a semantic gap between the model produced by the designer, the model used by the model-checker and the executable. For the Hippo tool chain, the code is generated as close as possible to the TTS (Time Transition Systems) model underlying Fiacre. Thus, during the generation step, a translator is used to produce, from a Fiacre model, a C code that guarantees a control flow identical in all points to the TTS behavior. During this presentation we will discuss these different steps and show how to use the tool on some concrete use cases.

We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.