Debian GNU/Linux is a Linux distribution composed of free and open-source software. It is heavily used all over the world as an operating system for personal computers and servers, and is the basis for many other distributions.

Deban currently includes more than 28 thousand maintainer scripts, almost all of them written in POSIX shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. While Debian policy provides guidance for package maintainers producing the scripts, few tools exist to check the compliance of a script to it.

This presentation reports on the application of a formal verification approach based on symbolic execution to find violations of some non-trivial properties required by Debian policy in maintainer scripts. We present our methodology and give an overview of the toolchain. We focus in particular on the tree logics used to represent symbolically a file system transformation, and the use of such a logic in the symbolic engine.

Communicating finite-state machines (CFMs) are a standard model of concurrent message-passing systems. They consist of a fixed number of finite-state processes communicating through unbounded point-to-point FIFO channels, and they define languages of partial orders called message sequence charts (MSCs), representing possible executions of the system. In this talk, I will review past and recent characterizations of the expressive power of CFMs, in the spirit of Büchi-Elgot-Trakhtenbrot theorem for finite automata. Our main result is that, both for finite and infinite executions, CFMs have the same expressive power as existential monadic second-order logic (EMSO). As a corollary, we obtain a new proof of a known characterization in the restricted case where the channels are assumed to be of bounded size, namely, that CFMs are equivalent to full MSO logic over finite existentially-bounded MSCs. We also extend that result from finite to infinite executions. For the main result, where channels are assumed to be unbounded, the proof relies on another logic of independent interest: a star-free variant of propositional dynamic logic based on operations similar to LTL “since” and “until” modalities. This logic is equivalent to first-order logic, and its formulas can be translated into equivalent CFMs of exponential size (on the other hand, the translation from first-order logic is non-elementary). This is joint work with Benedikt Bollig and Paul Gastin.

The control of the information given by a system has recently seen increasing importance due to the omnipresence of communicating systems, the need for privacy, etc. This control can be used in order to disclose to an observer an information of the system, or, oppositely, to hide one. In this talk, I will consider the control of the information released by a system represented by a stochastic model such as a Markov chain. Here, an external observer is interested in detecting a particular set of relevant paths of the system. However, he can only observe those paths through an observation function which obfuscates the real behaviour of the system. Exact disclosure of the information occurs when the observer can deduce from a finite observation that the path is relevant, the approximate disclosure variant corresponding to the path being identified as relevant with high accuracy. I will discuss the problems of diagnosability and opacity, which corresponds, in spirit, to the cases where one wants to disclose all the information or hide as much of it as possible with a focus on the approximate notion of disclosure.

We consider the problem of deciding ω-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent ω-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with “+”, each negative entry with “−”, and each zero entry with “0”) satisfies the given property. Our procedure requires that the recurrence be simple, \ie, that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Semënov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables. This is joint work with: Shaull Almagor, Toghrul Karimov, Jöel Ouaknine, and James Worrell.

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology of the system (e.g. pipeline, ring). Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires inferring an inductive invariant that contains all reachable states of all system instances and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. The invariants are defined using the WSkS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a WSkS formula. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.

If time allows, in the second part of this talk I will describe a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (mutual exclusion, absence of deadlocks).

In this talk I address the problem of finite-horizon probabilistic safety for discrete-time stochastic systems over general (uncountable or hybrid) state spaces. I show how to compute discrete-time, finite state Markov chains as formal abstractions of such systems. The abstraction differs from existing approaches in two ways. First, it exploits the structure of the underlying system to compute the abstraction separately for each dimension. Second, it employs dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements. I show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. Guaranteed bounds on the error in the abstraction can be computed with respect to the probabilistic safety property. Additionally, I show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic safety problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes. I will also briefly discuss two of the tools for Markov chain abstraction: FAUST2 and Amytiss.

We consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.

We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accomodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

Simple stochastic games are turn-based 2.5-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.

Consider 2-player perfect information turn-based stochastic games on finite or infinite graphs, and sub-cases (e.g., Markov decision processes (MDPs)). Depending on the objective of the game, optimal strategies (where they exist) and epsilon-optimal strategies may need to use a certain amount/type of memory or to use randomization. This is called the strategy complexity of the objective on the given class of games. We give an overview over the strategy complexity of common objectives on games and MDPs, with a particular focus on the differences between finite-state games/MDPs and infinite-state games/MDPs.

Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. With Anirban Majumdar and Patricia Bouyer, we introduced a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear finite-word languages to describe the possible move combinations that lead from one vertex to another.

We report on results on two problems for so-called parameterized concurrent games. To start with, we tackled the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. We establish the precise complexities of the parameterized reachability game problem. Second, we consider a synthesis problem, where one aims at designing a strategy for each of the players so as to achieve a common objective. For safety objectives, we show that this kind of distributed synthesis problem is decidable.

In this talk we survey the deterministic membership and deterministic separability problems for timed automata. In the deterministic membership problem (a.k.a. determinisability) we are given in input a nondeterministic timed automaton (NTA) and we have to decide whether there is a deterministic timed automaton (DTA) recognising the same language. In the deterministic separability problem, we are given in input two NTA and we have to decide whether there is a DTA separating them.

We survey decidability and undecidability results for these two problems and for their variants where we put restrictions on the number of clocks of the input NTA and/or the output DTA. While the deterministic separability problem has been studied before in the timed automata literature (mostly with undecidability results), the separability problem does not appear to have been addressed before.

There has been a great deal of work on local reasoning about state for proving the absence of bugs, but none for proving the presence of bugs. In this paper, we present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: (1) separation logic and (2) the recently introduced “incorrectness logic”. In addition to exploring the theory of this new incorrectness separation logic (ISL), we show how it can be used to derive a begin-anywhere, intra-procedural forward symbolic execution analysis that has no false positives by construction. In so doing, we take a step towards transferring modular, scalable techniques from the world of program verification to the world of bug catching.

For quadratic word equations, there exists an algorithm based on rewriting rules which generates a directed graph describing all solutions to the equation. For regular word equations – those for which each variable occurs at most once on each side of the equation – we investigate the properties of this graph, such as bounds on its diameter, size, and DAG-width, as well as providing some insights into symmetries in its structure. As a consequence, we obtain a combinatorial proof that the problem of deciding whether a regular word equation has a solution is in NP.

Recently, there is growing concern that machine-learning models, which currently assist or even automate decision making, reproduce, and in the worst case reinforce, bias of the training data. The development of tools and techniques for certifying fairness of these models or describing their biased behavior is, therefore, critical. In this paper, we propose a perfectly parallel static analysis for certifying causal fairness of feed-forward neural networks used for classification of tabular data. When certification succeeds, our approach provides definite guarantees, otherwise, it describes and quantifies the biased behavior. We design the analysis to be sound, in practice also exact, and configurable in terms of scalability and precision, thereby enabling pay-as-you-go certification. We implement our approach in an open-source tool and demonstrate its effectiveness on models trained with popular datasets.

Linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering, to model the evolution of a system over (discrete or continuous) time. Rechability analysis of such systems thus plays a key role in many areas of computer science, including program verification, abstract interpretation, robotic motion planning, and many more. Already for the simplest variants of linear dynamical systems, the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems.

In this talk, we introduce the class of o-minimal invariants, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-reachability for dynamical systems, equipped with a large class of halting conditions. In the discrete setting, we establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory. We then examine the continuous setting, and the challenges that arise there. We establish some decidability resutls, and some conditional decidability results. We also demonstrate the hardness of a remaining case, with respect to open problems in number theory.

Non-volatile memory (NVM) is emerging as a technology that may significantly impact the computing landscape in the near future. NVM ensures durability of data across power failures (i.e., as hard drives do) at a performance close to that of conventional volatile memory (RAM). Nevertheless, NVM is quite difficult to use correctly because of data caches: the writes do not persist to memory immediately when performed by a program and may further be reordered. In order to ensure that writes are propagated to memory in the correct order and that all writes have persisted to memory, the programmers have to use special barrier and cache flushing instructions.

The talk will discuss the semantics of such instructions, how they interact with the architecture's weak consistency model, and how they can be used to develop higher-level primitives for safe persistent programming.

I will present two recent results from my research group. First, I will show the notion of Brzozowski derivative of a formal language can be combined with the zipper data structure and used to construct efficient LL(1) parsers [1] (joint work with Romain Edelmann and Jad Hamza). Second, I will present System FR, an expressive dependent type system with refinement types and subtyping, whose design is guided by interpretation of types as sets of terms [2] (joint work with Jad Hamza and Nicolas Voirol), and which serves as foundation of Stainless verifier for Scala [3].

[1] http://lara.epfl.ch/~kuncak/paper/EdelmannETAL20ZippyLLParsingDerivatives.pdf [2] http://lara.epfl.ch/~kuncak/papers/HamzaETAL19SystemFR.pdf [3] https://stainless.epfl.ch/

I introduce and advocate for the concept of Real-Time Systems Compilation. By analogy with classical compilation, real-time systems compilation consists in the fully automatic construction of running, correct-by-construction implementations from functional and non-functional specifications of embedded control systems. Like in a classical compiler, the whole process must be fast (thus enabling a trial-and-error design style) and produce reasonably efficient code. This requires the use of fast heuristics, and the use of fine-grain platform and application models. Unlike a classical compiler, a real-time systems compiler must take into account non-functional properties of a system and ensure the respect of non-functional requirements (in addition to functional correctness). I also present Lopht, a real-time systems compiler we built by combining techniques and concepts from real-time scheduling, compilation, and synchronous languages.

I will present a few recent results about reachability problem for fixed dimensional VASSes. There results invalidate some previously posed conjectures and show that the problem is harder than previously expected to be.

This is a joint work with Sławomir Lasota, Ranko Lazic, Jerome Leroux and Filip Mazowiecki.

In this talk I will present some results we obtained in LICS 2018 where we exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of inde- pendent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.

I will then give a small introduction to algebraic geometry for computer scientisits. The goal it to give the background necessary to understand how the proof works: we will talk about algebraic sets/varieties and constructible/definable sets.

In a second talk on April 20th, I will give use the material introduced in this talk to explain the algorithm for computing the Zariski closure of a group and semigroup of matrices.

Solidity is the dominant programming language for smart contracts on the Ethereum blockchain. This talk presents a high-level formalization of the Solidity language with a focus on the memory model. The memory model of Solidity has various unusual and non-trivial behaviors, providing a fertile ground for potential bugs. Smart contracts have access to two classes of data storage: a permanent storage that is a part of the global blockchain state, and a transient local memory used when executing transactions. While the local memory uses a standard heap of entities with references, the permanent storage has pure value semantics (although pointers to storage can be declared locally). This memory model that combines both value and reference semantics - with all interactions between the two - poses some interesting challenges but also offers great opportunities for automation. The presented formalization covers all features of the language related to managing state and memory in an effective way: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify tool and we provide an evaluation on an extensive test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.

In this talk I will present some results we obtained in LICS 2018 where we exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of inde- pendent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.

I will then give a small introduction to algebraic geometry for computer scientisits. The goal it to give the background necessary to understand how the proof works: we will talk about algebraic sets/varieties and constructible/definable sets.

In a second talk on April 20th, I will give use the material introduced in this talk to explain the algorithm for computing the Zariski closure of a group and semigroup of matrices.

We study the expressiveness of polynomial recurrence sequences (PRS), a nonlinear extension of the well-known class of linear recurrence sequences (LRS). A typical example of a sequence definable in PRS but not in LRS is a_n = n!. Our main result is that the sequence u_n = n^n cannot be defined by any PRS. We also discuss the impact of our results on the expressiveness of nonlinear extensions of weighted automata. This is joint work with Michaël Cadilhac, Charles Paperman, Michał Pilipczuk and Géraud Sénizergues.

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, that is the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterizations in terms of Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Hence our work gives a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

Probabilistic Logics are formal languages designed to express properties of probabilistic programs. For most probabilistic logics several key problems are still open. One of such problems is to design convenient analytical proof systems in the style of Gentzen sequent calculus. This is practically important in order to simplify the task of proof search: the CUT-elimination theorem greatly reduces the search space. In this talk I will present some recent developments in this direction.

We study infinite games played on graphs, in which players move a token along the edges of a graph. Each player has certain preferences over the resulting infinite path taken by the token, and will choose their actions accordingly. In this setting, we are particularly interesting in Nash equilibria, which describe a course of action such that no player has any incentive to deviate and is thus seen as a rational outcome of the game. We add a communication mechanism to the classical setting, such that players can send information to and receive information from other players, and we show that the resulting Nash equilibria can be expressed with a very simple communication scheme, thus allowing us to design an algorithm to compute them.

It is becoming increasingly important to understand the vulnerability of machine learning models to adversarial attacks. In this talk, we will study the feasibility of robust learning from the perspective of computational learning theory, considering both sample and computational complexity. In particular, our definition of robust learnability requires polynomial sample complexity. We start with two negative results. We show that no non-trivial concept class can be robustly learned in the distribution-free setting against an adversary who can perturb just a single input bit. We show moreover that the class of monotone conjunctions cannot be robustly learned under the uniform distribution against an adversary who can perturb ω(log n) input bits. However if the adversary is restricted to perturbingO(log n) bits, then the class of monotone conjunctions can be robustly learned with respect to a general class of distributions (that includes the uniform distribution). Finally, we provide a simple proof of the computational hardness of robust learning on the boolean hypercube. Unlike previous results of this nature, our result does not rely on another computational model (e.g. the statistical query model) nor on any hardness assumption other than the existence of a hard learning problem in the PAC framework.

We consider the problem of deciding termination of linear constraint loops, that is, single-path loops in which the loop body consists of a (possibly non-deterministic) assignment, specified a conjunction of linear constraints. We present several versions of this problem, according to the syntactic form of the loop and the numerical domain of the program variables. We sketch some decidability results and point out open problems.

Unambiguous automata are a popular compromise between non-deterministic and deterministic automata in terms of succinctness and complexity. A word is called a killing word for an automaton if there is no path labelled by it in this automaton. Here we will discuss the problem of computing a short killing word for an unambiguous automaton, as well as possible extensions. Unambiguous automata are closely related to codes, and this problem can be viewed as a particular instance of Restivo's conjecture, a longstanding problem in the theory of codes. It can also be interpreted as a restricted version of the matrix mortality problem. This is a joint work with Stefan Kiefer, published at STACS 2019.

Processors cache data to avoid slow access to main memory. When a cache set is full, one block of data is evicted to make room for new data. A replacement policy chooses which block to evict. The most natural one is to evict the least recently used (LRU) block. It however had the reputation among hardware designers of being hard to implement, and thus they proposed some “pseudo LRU” policies supposed to behave “similarly”. There is also a FIFO policy, also easy to implement.

For safety critical systems it is sometimes necessary to prove bounds on the worst-case execution time by static analysis. This analysis has to take into account the cache system. There is a well known abstract interpretation for LRU caches, based on “ages”; no such analyses are known for other cache policies. Indeed, the common wisdom is that “pseudo LRU” caches are hard to analyse because their behavior may depend on events in the distant past that one cannot be sure to have flushed away.

In this talk: - We show how this common wisdom can be grounded in strong theory: we prove that, in a certain model, exact static analysis for two kinds of pseudo LRU caches and for FIFO is PSPACE-complete, while that for LRU is “only” NP-complete. - We give a practical algorithm for exact static analysis for LRU. This analysis has been implemented in the OTAWA tool.

Despite continued progress in program verification, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because these effects lead to non-deterministic behavior. Although many specialized logics have been developed to reason about programs that use either concurrency or randomization, most can only handle the use of one of these features in isolation. However, many common concurrent data structures are randomized, making it important to consider the combination.

This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel's denotational model of non-determinism and probability, (2) Barthe et al.'s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.