## Vérification

#### Jour, heure et lieu

Le lundi à 11h00, salle 1007

Le calendrier des séances (format iCal).

Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

#### Contact(s)

### Prochaines séances

Vérification

Lundi 22 avril 2024, 11 heures, 3052 and Zoom link

**Sidi Mohamed Beillahi** (University of Toronto) *Non encore annoncé.*

Vérification

Lundi 29 avril 2024, 11 heures, 3052 and Zoom link

**Niklas Kochdumper** (IRIF) *Non encore annoncé.*

Vérification

Lundi 27 mai 2024, 11 heures, 3052 and Zoom link

**Nicolas Amat** (IMDEA) *Non encore annoncé.*

### Séances passées

#### Année 2024

Vérification

Lundi 25 mars 2024, 11 heures, 3052 and Zoom link

**Étienne André** (LIPN) *Monitoring cyber-physical systems under uncertainty*

First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds. We rely on two solutions, one based on model-checking, and the other one being ad-hoc.

Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)—the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log.

We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant.

This presentation is mainly based on publications at ACM ToSEM (2023) ACM ToCPS (2022), and are joint work with Masaki Waga (Kyoto University) and Ichiro Hasuo (NII, Tokyo, Japan).

Vérification

Lundi 18 mars 2024, 11 heures, 3052 and Zoom link

**Sarah Winter** (IRIF) *Deterministic Regular Functions of Infinite Words*

This is joint work with Olivier Carton, Gaëtan Douéneau-Tabot, and Emmanuel Filiot.

Vérification

Lundi 11 mars 2024, 11 heures, 3052 and Zoom link

**Uli Fahrenberg** (LRE / EPITA) *Quantitative Verification: the Good, the Bad, the Ugly*

In order to ensure robustness of verification, we replace the Boolean yes-no answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. We develop such a general theory, using games with quantitative objectives to define a quantitative version of van Glebbeek's linear-time-branching-time spectrum.

We also extend this to a compositional theory of quantitative specifications, using disjunctive modal transition systems which capture precisely the greatest-fixed-point part of the mu-calculus, i.e. safety properties.

We currently do not know how to go beyond safety properties. Another major obstacle is that we do not know how to integrate silent transitions into our framework. Finally, we argue that quantitative verification of real-time and hybrid systems poses other challenges which force us to look beyond our framework.

The first 3/4 of this talk are based on the speaker's habilitation thesis which can be found at https://arxiv.org/abs/2204.11302 or https://hal.science/hal-04206693

Vérification

Lundi 4 mars 2024, 11 heures, 3052 and Zoom link

**Adrian Francalanza** (University of Malta) *An Operational Guide to Monitorability*

This is joint work with Luca Aceto, Antonis Achilleos, Anna Ingolfsdottir and Karoliina Lehtinen

Vérification

Lundi 26 février 2024, 11 heures, 3052 and Zoom link

**Loïc Germerie Guizouarn** (Université Paris-Est Créteil) *Quasi-synchronous communications and verification of distributed systems*

Vérification

Lundi 19 février 2024, 11 heures, 3052 and Zoom link

**Dylan Marinho** (Telecom SudParis) *Execution-time opacity problems in (parametric) timed automata*

Vérification

Lundi 12 février 2024, 11 heures, 3052 and Zoom link

**Jawher Jerray** (Télécom Paris) *Guaranteed properties of real-time systems under perturbations.*

Vérification

Lundi 5 février 2024, 11 heures, Zoom link

**Tayssir Touili** (LIPN) *On static malware detection*

Vérification

Lundi 15 janvier 2024, 11 heures, 3052 and Zoom link

**Raphaël Berthon** (Aachen University) *Natural Strategic Ability in Stochastic Multi-Agent Systems*

Vérification

Lundi 8 janvier 2024, 11 heures, 3052 and Zoom link

**Henry Sinclair-Banks** (University of Warwick) *Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality*

#### Année 2023

Vérification

Lundi 18 décembre 2023, 11 heures, 3052 and Zoom link

**Munyque Mitteelmann** (University of Naples Federico II) *Logics for Strategic Reasoning: Recent Developments and Application to Mechanism Design*

Vérification

Lundi 4 décembre 2023, 11 heures, 3052 and Zoom link

**Marco Campion** (INRIA) *Monotonicity and the Precision of Program Analysis*

Vérification

Lundi 20 novembre 2023, 11 heures, Zoom link

**Rômulo Meira Goes** (The Pennsylvania State University) *On securing the next generation of critical infrastructure systems: A discrete event systems approach*

Vérification

Lundi 6 novembre 2023, 11 heures, 3052 and Zoom link

**Bernardo Jacobo Inclán** (IRIF) *Bandwidth of Timed Automata: 3 classes*

In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log (1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these 3 classes of bandwidth, implying that there are no intermediate asymptotic classes.

Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri's orbit graphs, and the proofs are based on Simon's factorization forest theorem.

Joint work with E. Asarin, A.Degorre, C.Dima

Vérification

Lundi 16 octobre 2023, 11 heures, 3052 and Zoom link

**Lucie Guillou** (IRIF) *Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous*

Vérification

Lundi 9 octobre 2023, 11 heures, 3052 and Zoom link

**Emily Clément** (IRIF) *Layered controller synthesis for dynamic multi-agent systems.*

Vérification

Lundi 25 septembre 2023, 11 heures, 3052 and Zoom link

**Masaki Waga** (Kyoto University) *Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization.*

Vérification

Lundi 26 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Adrian Francalanza** (University of Malta) *If At First You Don’t Succeed: Extended Monitorability through Multiple Executions*

Vérification

Lundi 19 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Mohammed Foughali** (IRIF) *Compositional Verification of Embedded Real-Time Systems*

Vérification

Lundi 12 juin 2023, 11 heures, Olympe de Gouges 147 and Zoom link

**Themistoklis Melissourgos** (University of Essex) *Strong Inapproximability Results on Pizza-Sharing*

Joint work with Argyrios Deligkas and John Fearnley.

Vérification

Lundi 5 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Pedro Ribeiro** (University of York) *Co-verification for robotics: simulation and verification by proof*

Vérification

Lundi 22 mai 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Igor Walukiewicz** (CNRS, Bordeaux University) *Active learning deterministic negotiations*

Deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure together with the assumption of deadlock freedom allows minimizing such negotiations.

Angluin's L* algorithm can learn a regular language with polynomialy many queries to Teacher. Active learning algorithms have been designed for many extensions of deterministic finite automata. The challenge in adapting this approach to negotiations is in extracting relevant information from a Teacher's answer: if a teacher says that an execution should not be accepted, it is not clear which parallel component in a negotiation should be modified.

We present a learning algorithm whose complexity, measured in the number of queries to the Teacher, is practically the same as the standard algorithm for finite automata. This is interesting, as a finite automaton representing a negotiation can be exponentially bigger than the negotiation.

Vérification

Lundi 15 mai 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Salim Chehida** (Université Grenoble Alpes) *A Formal MDE Framework for Inter-DSL Collaboration*

Vérification

Mardi 9 mai 2023, 14 heures, Olympe de Gouges 146 and Zoom link

**Stéphane Gaubert** (INRIA and CMAP, Ecole polytechnique, IP Paris, CNRS) *Universal Complexity Bounds Based on Value Iteration for Stochastic Games and Entropy Games*

Vérification

Lundi 17 avril 2023, 11 heures, Olympe de Gouges 146 and Zoom link

**Björn Brandenburg** (MPI SWS) *PROSA: Trustworthy Schedulability Analysis for Safety-Critical Real-Time Systems*

However, how much *trust* should we place in the results of a schedulability analysis, and more generally, results obtained with formal methods, in the certification of critical systems? Using schedulability analysis as a specific example, I will examine several ways in which analysis results might be unsound or otherwise unsatisfying and argue that there is ample room for reasonable doubt. However, that begs the question: why should industry practitioners adopt methods conceived to increase confidence in a system's (temporal) correctness if these methods are not so confidence-inspiring after all?

Formal verification offers a path out of this conundrum. While the implied effort and learning curve may initially seem off-putting, I will argue that it is, in fact, both viable and desirable to verify schedulability analyses formally. As a proof of concept, I will present PROSA, a Coq framework for machine-checked schedulability analysis, which we have been developing since 2015. Out of the box, PROSA provides machine-checked and hence *trustworthy* schedulability analyses suitable for use in critical systems. Additionally, PROSA has enabled us to find more general results and derive explainable analyses, as I will explain in my talk.

Finally, I will report on two ongoing projects, one seeking to close the “model gap” between PROSA and a system's codebase and one aiming to enable mathematically sound below-worst-case provisioning.

Vérification

Lundi 3 avril 2023, 11 heures, 1007 and Zoom link

**Thomas Nowak** (ENS Paris-Saclay) *Reaching Consensus in Hostile Environments*

Vérification

Lundi 27 mars 2023, 11 heures, 1007 and Zoom link

**Lénaïg Cornanguer & Christine Largouët** (IRISA Rennes) *TAG: Learning Timed Automata from Logs*

We consider real-time systems, which can be modeled with Timed Automata: our approach is thus a Timed Automata learner. There is a handful of related work, however, they might require a lot of parameters or produce Timed Automata that either are undeterministic or lack precision. In contrast, we propose an approach, called TAG, that requires only one parameter and learns, without any a-priori knowledge, a deterministic Timed Automaton having a good tradeoff between accuracy and automata complexity. This allows getting an interpretable and accurate global model of the considered real-time system. Experiments compare our approach to related work and demonstrate its merits.

Vérification

Lundi 20 mars 2023, 11 heures, 1007 and Zoom link

**Eric Munday** (University of Edinburgh) *Strategy complexity of lim sup in countable MDPs*

Vérification

Lundi 13 mars 2023, 11 heures, 1007 and Zoom link

**Daniel Neider** (TU Dortmund) *Reinforcement Learning with (Stochastic) Reward Machines*

In this presentation, we will survey recent approaches that intertwine reinforcement learning and the inference of reward machines, thereby eliminating the need to craft a reward machine by hand. At their heart, these methods transform the inference task into a series of constraint satisfaction problems that can be solved using off-the-shelf SAT and SMT solvers. We will see how this idea can be used to integrate user-provided advice into the learning process and how it deals with stochastic reward signals. Moreover, we will briefly discuss theoretical properties and hint at empirical evidence demonstrating that reinforcement learning with reward machines outperforms existing methods, such as hierarchical and deep reinforcement learning.

Vérification

Lundi 6 mars 2023, 11 heures, 1007 and Zoom link

**Thomas Chatain** (ENS Paris-Saclay) *Towards Conformance Checking for Timed Process Models*

The subject of this work is to study conformance checking for timed models, that is, process models that consider both the sequence of events in a process as well as the timestamps at which each event is recorded. We set our problem of timed alignment and solve two cases, each corresponding to a different metric over timed traces.

Vérification

Lundi 20 février 2023, 11 heures, 1007 and Zoom link

**Kevin Zagalo** (Inria Paris) *Schedulability of stationary real-time systems*

Vérification

Lundi 13 février 2023, 11 heures, 1007 and Zoom link

**Rémi Morvan** (LaBRI) *Universal algorithms for parity games and nested fixpoints*

The first quasi-polynomial algorithm was found in 2017. Soon after, McNaughton-Zielonka algorithm (an exponential-time recursive algorithm, which is arguably one of the simplest algorithm for solving parity games, and the most effective in practice) was tweaked, first by Parys and then by Lehtinen, Schewe and Wojtczak, to run in quasipolynomial time. In some sense, these algorithms forces McNaughton-Zielonka algorithm to skip enough recursive calls as to run in quasipolynomial time, but not too much so that the output remains correct. We introduce a meta-algorithm that solves parity games, parametrized by trees, which will precisely guide the recursive call made by the algorithm, and show that the output is correct when the trees satisfy some combinatorial property called universality, introduced by Fijalkow and co-authors. McNaughton-Zielonka algorithm and variations can all three be seen as an instantiation of this meta-algorithm on particular classes of universal trees.

I will also emphasize and reformulate these ideas in the slightly more general context of nested fixpoints over finite lattices, and show that these algorithms can be turned into symbolic algorithm that only uses logarithmic symbolic space. The talk is mainly based on a joint work with Marcin Jurdziński and K. S. Thejaswini. The results were proven independently by André Arnold, Damian Niwiński and Paweł Parys, for nested fixpoints.

Vérification

Lundi 6 février 2023, 11 heures, 1007 and Zoom link

**Claudio Gomes** (University of Aarhus) *Application of formal methods to verification of self-adaptation loops in digital twins*

Vérification

Lundi 30 janvier 2023, 11 heures, 1007 and Zoom link

**Sylvain Perifel** (IRIF) *Deterministic pushdown automata can compress some normal sequences*

Normality has been introduced by É. Borel more than one hundred years ago. A real number is normal to an integer base if, in its infinite expansion expressed in that base, all blocks of digits of the same length have the same limiting frequency. Normality can also be characterized by non-compressibility by finite state machines. In this talk, we will present a new result showing that pushdown machines, even deterministic, can compress some normal sequences. This solves positively a question left open by V. Becher, P. A. Heiber and O. Carton.

Vérification

Lundi 30 janvier 2023, 11 heures, 3052 and Zoom link

**Sarah Winter** (IRIF) *Non encore annoncé.*

Vérification

Lundi 23 janvier 2023, 11 heures, 1007 and Zoom link

**Stefan Kiefer** (University of Oxford) *On the state complexity of complementing unambiguous finite automata*

Online seminar streamed in room 1007.

Vérification

Lundi 16 janvier 2023, 11 heures, 1007 and Zoom link

**Benjamin Bordais** (LMF) *Playing (almost-)optimally in concurrent games with reachability, Büchi and co-Büchi objectives*

Concurrent games are more general than their turn-based counterparts in which, at each state, only one player chooses the next state to visit. However, this comes at the cost of not enjoying the desirable properties that turn-based games do. (For instance, in turn-based games with the parity objective, there are always optimal strategies that are pure and positional whereas optimal strategies do not exist in general in concurrent games.) In this talk, I will illustrate the turn-based and concurrent formalisms and show on specific examples why concurrent games behave more poorly than turn-based games. Then I will present how to build concurrent games that are more general than turn-based games but still enjoy similar properties that turn-based game do for specific objectives, namely reachability, Büchi and co-Büchi. This is a joint work with my PhD supervisors Patricia Bouyer and Stéphane Le Roux.

Vérification

Lundi 9 janvier 2023, 11 heures, 1007 and Zoom link

**Petr Novotný** (Masaryk University) *Formal methods meet Monte Carlo tree search*

Online seminar streamed in room 1007.

#### Année 2022

Vérification

Lundi 12 décembre 2022, 11 heures, 1007 and Zoom link

**Salim Chouai** (Mohammed VI University) *Synthesis of Accuracy Specification under Differential Privacy*

Vérification

Lundi 5 décembre 2022, 11 heures, 1007 and Zoom link

**Kohei Suenaga** (Kyoto University) *HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types*

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.

Vérification

Lundi 28 novembre 2022, 11 heures, 1007 and Zoom link

**Nicolas Waldburger** (IRISA − Université de Rennes 1) *Parameterized Safety Verification of Round-Based Shared-Memory Systems*

Vérification

Lundi 21 novembre 2022, 11 heures, 1007 and Zoom link

**Eric Goubault** (École Polytechnique) *Verification of neural nets by abstract interpretation*

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.

Vérification

Lundi 14 novembre 2022, 11 heures, 1007 and Zoom link

**Philip Offtermatt** (Université de Shrebrooke) *The Complexity of Soundness in Workflow Nets*

Vérification

Lundi 7 novembre 2022, 11 heures, 3052 and Zoom link

**Lorenzo Clemente** (University of Warsaw) *Zeroness and equality problems for weighted register automata over equality data*

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.

Vérification

Lundi 24 octobre 2022, 11 heures, 1007 and Zoom link

**Govind R** (IIT Bombay) *Simulations for Event-Clock Automata*

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.

Vérification

Mardi 18 octobre 2022, 16 heures, 1007 and Zoom link

**Edon Kelmendi** (MPI) *The Set of Positive Entries of a Linear Recurrence Sequence*

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.

Vérification

Lundi 10 octobre 2022, 11 heures, 3052 and Zoom link

**Cristina Seceleanu** (Mälardalen University) *Reinforcement Learning for Mission Plan Synthesis of Autonomous Vehicles*

Vérification

Lundi 19 septembre 2022, 11 heures, 3052 and Zoom link

**Shachar Itzhaky** (Technion University) *TheSy: Theory Exploration Powered by Deductive Synthesis and E-graphs*

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.

Joint session with the PPS seminar.

Vérification

Lundi 11 juillet 2022, 11 heures, 3052 and Zoom link

**Jaco Van De Pol** (Aarhus University) *Parallel SCC Detection for Model Checking – Model Checking for Parallel SCC detection*

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.

Vérification

Lundi 4 juillet 2022, 11 heures, 1007 and Zoom link

**Radosław Piórkowski** (Universit of Warsaw) *Synthesis games over infinite alphabets*

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.

Vérification

Lundi 27 juin 2022, 11 heures, 3052 and Zoom link

**[Cancelled] Nicolas Waldburger** (IRISA − Université de Rennes 1) *Parameterized Safety Verification of Round-Based Shared-Memory Systems*

Vérification

Lundi 20 juin 2022, 11 heures, 3052 and Zoom link

**Mahsa Shirmohammadi** (IRIF − CNRS) *Learning Weighted Automata over PIDs*

Vérification

Lundi 30 mai 2022, 11 heures, 3052 and Zoom link

**Miquel Oliu-Barton** (Université Paris-Dauphine and Bruegel) *New algorithms for solving zero-sum stochastic games*

Vérification

Lundi 16 mai 2022, 11 heures, 3058 and Zoom link

**Klara Nosan** (IRIF) *The Membership Problem for Hypergeometric Sequences with Rational Parameters.*

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>.

Vérification

Lundi 9 mai 2022, 11 heures, Zoom link

**James Worrell** (University of Oxford) *The Skolem Landscape*

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

Vérification

Lundi 11 avril 2022, 11 heures, 3052 and Zoom link

**Aldric Degorre** (IRIF − Université Paris Cité) *On the bandwidth of timed automata*

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.

This is an “Open Talk” session of the seminar.

Open talk sessions are dedicated to present one or several ongoing works from verification team members or their students: - just for showing what they are currently doing, - for sharing a new result, - to ask a scientific question to the audience, - to listen to comments and ideas related to presented research - or looking for somebody to work with.

Vérification

Lundi 28 mars 2022, 11 heures, Zoom link

**Moses Ganardi** (Max Planck Institute for Software Systems (MPI-SWS)) *Balancing in Grammar-Based Compression*

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

Vérification

Lundi 14 mars 2022, 11 heures, Zoom link

**Ruiwen Dong** (University of Oxford) *The identity problem for unitriangular matrices of dimension four.*

Vérification

Lundi 7 mars 2022, 11 heures, Zoom link

**Bernd Finkbeiner** (CISPA Helmholtz Center for Information Security, Universität des Saarlandes) *Model Checking Hyperproperties*

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.

Vérification

Lundi 28 février 2022, 11 heures, 3052 and Zoom link

**Pierre-Emmanuel Hladik** (LS2N/Université de Nantes) *An Informal Presentation of Formal-Model Execution Engine Hippo to Control and Verify Critical Real-Time Systems*

Vérification

Lundi 31 janvier 2022, 11 heures, Zoom link

**Corto Mascle** (LABRI) *Responsibility and verification: Importance value in temporal logics*

#### Année 2021

Vérification

Lundi 13 décembre 2021, 11 heures, Zoom link

**Angelo Ferrando** (University of Genova) *Towards Runtime Verification of ROS applications*

Vérification

Lundi 6 décembre 2021, 11 heures, 1007 and Zoom link

**Alessio Mansutti** (University of Oxford) *Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic*

Vérification

Lundi 22 novembre 2021, 11 heures, 3058 and Zoom link

**Patricia Bouyer-Decitre** (FML - CNRS) *On the (Approximate) Analysis of Stochastic Real-Time Systems*

This talk is proposed in the context of the ANR project MAVeriQ day.

Vérification

Lundi 18 octobre 2021, 11 heures, 3052 and Zoom link

**Florian Renkin** (LRDE, EPITA) *Practical “Paritizing” of Emerson-Lei Automata*

Séminaire qui peut aussi intéresser l'équipe Automates

Vérification

Lundi 27 septembre 2021, 11 heures, 1007 and Zoom link

**Paula Herber** (University of Münster) *Contract-based Verification of Hybrid Simulink Models with Differential Dynamic Logic*

Vérification

Lundi 13 septembre 2021, 11 heures, 3052 and BBB link

**Lukáš Holík** (Brno University of Technology) *Regex matching with counting-set automata*

Vérification

Lundi 5 juillet 2021, 11 heures, 3052 and BBB link

**Eugène Asarin** (IRIF, Université de Paris) *On the complexity of timed pattern matching*

Timed pattern matching consists in finding occurrences of a timed regular expression in a timed word. This problem has been addressed using several techniques, its solutions are implemented in tools (quite efficient in practice), and used, for example in log analysis and runtime verification. In this work, we explore computational complexity of timed pattern matching, and prove P, NP and PSPACE bounds, depending on connectives used in expressions and other details. We conclude with a couple of open questions.

Vérification

Lundi 28 juin 2021, 11 heures, BBB link

**Emmanuel Filiot** (Université Libre de Bruxelles) *On Some Transducer Synthesis Problems*

Vérification

Lundi 14 juin 2021, 11 heures, 3052 and BBB link

**Arnaud Sangnier** (IRIF, Université de Paris) *Reachability in Distributed Memory Automata*

This is a joint work with Benedikt Bollig and Fedor Ryabinin.

We try an hybrid session. Dependending on technicalities, the visioconference platform may change.

Vérification

Lundi 7 juin 2021, 11 heures, BBB link

**Bernadette Charron-Bost** (LIX, École Polytechnique) *Foundational Aspects of the Blockchain Consensus*

In this talk we formulate such fundamental properties of the blockchain —“common prefix”, “chain quality”, “chain growth”— and show how the blockchain consensus differs from the classical problem of consensus in distributed computing and from the consensus in control theory. We analyze the impact of different setups, computational assumptions, and network models on the various properties of the blockchain consensus. We also examine the crucial role of the “proofs of work” for achieving network synchrony on top of unstructured P2P networks.

Vérification

Lundi 17 mai 2021, 11 heures, BBB link

**Sidi Mohamed Beillahi** (IRIF) *Checking Robustness Between Weak Transactional Consistency Models*

This a joint work with Ahmed Bouajjani and Constantin Enea.

Vérification

Lundi 10 mai 2021, 11 heures, BBB link

**Laurent Doyen** (LMF — ENS Saclay) *Observation and Distinction. Representing Information in Infinite Games*

The indistinguishability-relation model turns out to be strictly more expressive than the one based on observations. We present a characterisation of the indistinguishability relations that admit a representation as a finite-state observation function. We show that the characterisation is decidable, and give a procedure to construct a corresponding Mealy machine whenever one exists.

The talk is based on joint work with Dietmar Berwanger.

Vérification

Lundi 12 avril 2021, 11 heures, BBB link

**Jérôme Leroux** (LABRI) *Flat Petri nets*

In this presentation, we survey results about the reachability problem focusing on flat VASS. This subclass is central for computing the reachability set of general VASS using Presburger arithmetic. In fact, the reachability set of a VASS is Presburger if, and only if, it is flattable, i.e. the computation of its reachability set is reducible to the computation of the reachability set of a flat VASS. Whereas the reachability problem for flat VASS is clearly NP-complete in any fix dimension when numbers are encoded in binary, finding the exact complexity of the reachability problem for flat VASS in unary is a difficult (still open) problem.

Vérification

Lundi 22 mars 2021, 11 heures, BBB link

**James Worrell** (University of Oxford) *Dynamical Systems and Program Analysis*

Vérification

Lundi 15 mars 2021, 11 heures, BBB link

**Stefan Kiefer** (University of Oxford) *How to play in infinite MDPs*

Video available here https://www.youtube.com/watch?v=OFXkmtbgPUo

Vérification

Lundi 1 mars 2021, 11 heures, BBB link

**Mahsa Shirmohammadi** (IRIF, CNRS) *Cyclotomic Identity Testing and Applications*

Vérification

Jeudi 25 février 2021, 16 heures, BBB link

**Shaz Qadeer** (Novi Research, Seattle) *Reifying Concurrent Programs*

I will present Civl, a reifier for concurrent programs. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, consensus protocol, and shared-memory data structures. Civl is publicly available: https://civl-verifier.github.io/ <https://urldefense.com/v3/__https://civl-verifier.github.io/__;!!Bt8RZUm9aw! qKTqOLle9YgX-8Gw34-e9p0Q-WK9m5O2nhT_lXrSd7jSxOY4hpht0zir8Q$>.

This work has been done jointly with Bernhard Kragl (IST Austria).

Vérification

Lundi 22 février 2021, 11 heures, BBB link

**Mohammed Foughali** (Vérimag, Université Grenoble-Alpes) *On the formal verification of safety-critical systems: challenges, approaches and perspectives*

Vérification

Lundi 15 février 2021, 11 heures, BBB link

**Martin Helfrich** (Technical University of Munich) *Succinct Population Protocols for Presburger Arithmetic*

Vérification

Lundi 8 février 2021, 11 heures, BBB link

**Blaise Genest** (IRISA (CNRS)) *Global PAC Bounds for Learning Discrete Time Markov Chains.*

In this work, we provide global bounds on the error made by such a learning process, in terms of global behaviors formalized using temporal logic. More precisely, we propose a learning process ensuring a bound on the error in the probabilities of these properties. While such learning process cannot exist for the full LTL logic, we provide one ensuring a bound that is uniform over all the formulas of CTL. Further, given one time-to-failure property, we provide an improved learning algorithm. Interestingly, frequency estimation is sufficient for the latter, while Laplace smoothing is needed to ensure non-trivial uniform bounds for the full CTL logic.

Vérification

Lundi 1 février 2021, 11 heures, BBB link

**François Schwarzentruber** (IRISA, ENS Rennes) *Connected multi-agent path finding*

Vérification

Lundi 18 janvier 2021, 11 heures, BBB link

**Léo Henry** (IRISA, Université de Rennes I) *Active learning of timed automata with unobservable resets*

Vérification

Lundi 11 janvier 2021, 11 heures, BBB link

**Mohamed Faouzi Atig** (Uppsala University) *Parameterized verification under TSO is PSPACE-complete.*

#### Année 2020

Vérification

Lundi 14 décembre 2020, 11 heures, BBB link

**Nicolas Jeannerod** (IRIF) *Analysing installation scenarios of Debian packages*

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.

TACAS 2020 paper.

Vérification

Lundi 7 décembre 2020, 11 heures, BBB link

**Marie Fortin** (University of Liverpool) *Logics and automata over infinite message sequence charts*

Vérification

Lundi 30 novembre 2020, 11 heures, BBB link

**Engel Lefaucheux** (Max-Planck Institute for Software Systems, Sarrebrucken) *On Information Control in Probabilistic Systems: a closer look on Opacity and Diagnosis*

Vérification

Lundi 23 novembre 2020, 11 heures, BBB link

**Edon Kelmendi** (University of Oxford) *Deciding ω-Regular Properties on Linear Recurrence Sequences*

Vérification

Lundi 16 novembre 2020, 11 heures, BBB link

**Radu Iosif** (Verimag, CNRS) *Structural Invariants for the Verification of Systems with (Recursively Defined) Parameterized Architectures*

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).

Vérification

Lundi 9 novembre 2020, 11 heures, BBB link

**Sadegh Soudjani** (School of Computing, Newcastle University) *Formal verification of stochastic systems using Markov chains and dynamic Bayesian networks*

Video available here: https://www.youtube.com/watch?v=JrIcs2NY4OI

Vérification

Lundi 2 novembre 2020, 11 heures, BBB link

**Damien Busatto** (Université Libre de Bruxelles) *Monte Carlo Tree Search guided by Symbolic Advice for MDPs*

Vérification

Lundi 19 octobre 2020, 11 heures, BBB link

**Catalin Dima** (LACL, Université Paris-Est Créteil) *A Hennessy-Milner Theorem for ATL with Imperfect Information*

LICS 2020 paper

Vérification

Lundi 13 juillet 2020, 11 heures, (online, using BigBlueButton)

**Jan Kretinsky** (Technical University of Munich) *Approximating Values of Generalized-Reachability Stochastic Games*

Vérification

Lundi 6 juillet 2020, 11 heures, (online, using BigBlueButton)

**Richard Mayr** (University of Edinburgh) *Strategy Complexity: Finite Systems vs. Infinite Systems*

Vérification

Lundi 29 juin 2020, 11 heures, (online, using BigBlueButton)

**Nathalie Bertrand** (INRIA Rennes) *Games with arbitrarily many players*

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.

Vérification

Lundi 22 juin 2020, 11 heures, (online, using BigBlueButton)

**Lorenzo Clemente** (Warsaw university) *Deterministic membership and separability problems for timed automata*

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.

Vérification

Lundi 15 juin 2020, 11 heures, (online, using BigBlueButton)

**Azalea Raad** (Imperial College London) *Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic*

Vérification

Lundi 8 juin 2020, 11 heures, (online, using BigBlueButton)

**Joel Day** (Loughborough University) *On the structure of solution sets to regular word equations.*

Vérification

Mercredi 3 juin 2020, 14 heures, (online, using BigBlueButton)

**Caterina Urban** (INRIA- ENS) *Perfectly Parallel Fairness Certification of Neural Networks*

Vérification

Lundi 25 mai 2020, 11 heures, (online, using BigBlueButton)

**Shaull Almagor** (Technion Computer Science Faculty) *O-minimal invariants for discrete and continuous linear dynamical systems*

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.

Vérification

Lundi 18 mai 2020, 11 heures, (online using BigBlueButton)

**Viktor Vafeiadis** (MPI) *Semantics for Persistent Memory*

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.

Vérification

Lundi 11 mai 2020, 11 heures, (online, using BigBlueButton)

**Viktor Kuncak** (EPFL) *Deriving Parsers, Deriving Type Systems*

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

Vérification

Lundi 4 mai 2020, 11 heures, (online, using BigBlueButton)

**Dumitru Potop-Butucaru** (INRIA Paris) *Real-time systems compilation*

Vérification

Lundi 27 avril 2020, 11 heures, (online, using BigBlueButton)

**[Rescheduled] Wojciech Czerwinski** (University of Warsaw) *Reachability problem for fixed dimensional VASSes*

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

Vérification

Lundi 20 avril 2020, 11 heures, (online, using BigBlueButton)

**Amaury Pouly** (CNRS & IRIF) *Polynomial Invariants for Affine Programs and Introduction to Algebraic Geometry (for computer scientists)*

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.

Vérification

Mercredi 15 avril 2020, 15 heures, (online, using BigBlueButton)

**Akos Hajdu** (Budapest University of Technology and Economics) *SMT-Friendly Formalization of the Solidity Memory Model*

Vérification

Lundi 6 avril 2020, 11 heures, (online, using BigBlueButton)

**Amaury Pouly** (CNRS & IRIF) *Polynomial Invariants for Affine Programs and Introduction to Algebraic Geometry (for computer scientists)*

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.

Vérification

Lundi 30 mars 2020, 11 heures, (online, using BigBlueButton)

**[Rescheduled] Filip Mazowiecki** (MPI SWS) *Lower bounds for polynomial recurrence sequences*

Vérification

Lundi 30 mars 2020, 11 heures, Salle 1007

**[Cancelled] Adrian Francalanza** (University of Malta) *An Operational Guide to Monitorability*

Vérification

Lundi 16 mars 2020, 11 heures, Salle 1007

**[Cancelled] Matteo Mio** (CNRS & ENS de Lyon) *Towards a Proof Theory of Probabilistic Logics*

Vérification

Lundi 9 mars 2020, 11 heures, Salle 1007

**Nathan Thomasset** (LSV & ENS de Scalay) *Nash equilibria in games on graphs equipped with a communication mechanism*

Vérification

Lundi 2 mars 2020, 11 heures, Salle 1007

**Pascale Gourdeau** (University of Oxford) *On the hardness of robust classification*

Vérification

Lundi 24 février 2020, 11 heures, Salle 1007

**James Worrell** (University of Oxford) *Termination of linear constraint loops*

Vérification

Lundi 17 février 2020, 11 heures, Salle 1007

**Corto Mascle** (ENS de Cachan) *On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words*

Vérification

Lundi 10 février 2020, 11 heures, Salle 1007

**David Monniaux** (University of Grenoble.) *“Easy” vs hard analysis for caching policies*

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.

Vérification

Vendredi 10 janvier 2020, 10 heures, Salle 3052

**Joseph Tassarotti** (Boston College) *Verifying Concurrent Randomized Programs*

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.

Joint session between the PPS and Verification seminars.

#### Année 2019

Vérification

Lundi 16 décembre 2019, 11 heures, Salle 1007

**Jules Villard** (Facebook) *The Infer Static Analysis platform*

This talk will present how Infer is used at Facebook, where it analyses thousands of code changes every month, leading to thousands of bugs being found and fixed before they reach users. We will then see how to write your own inter-procedural static analysis in just a few lines of code inside Infer, and automatically be able to apply it to millions of lines of code.

Vérification

Mercredi 11 décembre 2019, 11 heures, Salle 1007

**Yotam Feldman** (Tel Aviv University) *Complexity and Information in Invariant Inference*

We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class.

We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries.

Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.

Joint work with Neil Immerman, Mooly Sagiv, and Sharon Shoham, that will appear in POPL'20.

Vérification

Lundi 9 décembre 2019, 11 heures, Salle 1007

**Sidi Mohamed Beillahi** (IRIF) *Checking Robustness Against Snapshot Isolation*

In this talk, we address the issue of verifying if a given program is robust against snapshot isolation, i.e., all its behaviors are serializable even if it is executed over a database ensuring snapshot isolation. We show that this verification problem is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. This reduction opens the door to the reuse of the classic verification technology for reasoning about sequentially-consistent programs. In particular, we show that it can be used to derive a proof technique based on Lipton's reduction theory that allows to prove programs robust.

This is a joint work with Ahmed Bouajjani and Constantin Enea.

Vérification

Vendredi 29 novembre 2019, 14 heures 30, Salle 3052

**Dmitry Chistikov** (University of Warwick) *On the complexity of linear arithmetic theories over the integers*

In this talk, I will survey constructions and ideas that underlie known answers to these questions, from classical results to recent developments, and open problems.

First, we will recall the geometry of integer linear programming and how it interacts with quantifiers. This will take us from classical results due to von zur Gathen and Sieveking (1978), Papadimitriou (1981), and others to the geometry of the set of models of quantified logical formulas. We will look at rational convex polyhedra and their discrete analogue, hybrid linear sets (joint work with Haase (2017)), and see, in particular, how the latter form a proper sub-family of ultimately periodic sets of integer points in several dimensions (the semi-linear sets, introduced by Parikh (1961)).

Second, we will discuss “sources of hardness”: which aspects of the expressive power make decision problems for logics over the integers hard. Addition and multiplication combined enable simulation of arbitrary Turing machines, and restriction of multiplication to bounded integers corresponds to resource-bounded Turing machines. How big can these bounded integers be in Presburger arithmetic? This leads to the problem of representing big numbers with small logical formulae, and we will see constructions by Fischer and Rabin (1974) and by Haase (2014). We will also look at the new “route” for expressing arithmetic progressions (in the presence of quantifier alternation) via continued fractions, recently discovered by Nguyen and Pak (2017).

Vérification

Vendredi 29 novembre 2019, 11 heures, Salle 3052

**Suresh Jagannathan** (Purdue University) *Mergeable Replicated Data Types*

This is joint work with Gowtham Kaki, Swarn Priya, and KC Sivaramakrishnan.

Vérification

Lundi 18 novembre 2019, 11 heures, Salle 1007

**Arnaud Sangnier** (IRIF) *The Complexity of Flat Freeze LTL*

Vérification

Vendredi 15 novembre 2019, 14 heures 30, Salle 3052

**Patrick Totzke** (Liverpool University) *Timed Basic Parallel Processes*

The first one describes “punctual” reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata. The other is a “sweep line” construction to compute optimal time to reach in reachability games played on one-clock TA.

Together, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.

This is joint work with Lorenzo Clemente and Piotr Hofman, and was presented at CONCUR'19. Full details are available at https://arxiv.org/abs/1907.01240.

Vérification

Lundi 4 novembre 2019, 11 heures, Salle 1007

**Zeinab Nehaï** (IRIF) *Deductive Proof of Industrial Smart Contracts Using Why3*

Vérification

Lundi 28 octobre 2019, 11 heures, Salle 1007

**Pierre Ganty** (IMDEA Software Institute) *Deciding language inclusion problems using quasiorders*

Vérification

Lundi 21 octobre 2019, 11 heures, Salle 1007

**Mohamed Faouzi Atig** (Uppsala University) *On Solving String Constraints*

Vérification

Lundi 14 octobre 2019, 11 heures, Salle 1007

**Laurent Doyen** (LSV, ENS Paris-Saclay) *Expected Finite Horizon*

A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon T, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.

Vérification

Lundi 23 septembre 2019, 11 heures, Salle 1007

**Stefan Kiefer** (University of Oxford) *Selective monitoring*

Vérification

Vendredi 5 juillet 2019, 14 heures 30, Salle 1001

**Mahsa Shirmohammadi** (IRIF) *Büchi Objectives in Countable MDPs*

Joint Automata & Verification Seminars

Vérification

Lundi 1 juillet 2019, 14 heures, Salle 3052

**Nikhil Balaji** (University of Oxford) *The complexity of some easy subclasses of the Skolem problem*

This algorithmic question has remained open despite several decades of active research, with decidability known only for a few restricted subclasses, by either restricting the depth of the LRS (up to 4) or by restricting the structure of the LRS (especially roots of the characteristic polynomials). Recent work due to Ouaknine and Worrell has shown that decidability of closely related algorithmic questions could entail significant breakthroughs in Diophantine approximation.

In this talk, we first present an elementary proof that this problem is NP-hard (which was already observed by Blondel and Portier). We further study some easy subclasses which are known to be decidable from the point of view of proving better complexity upper bounds. We are able to show that for a wide class of special cases of LRS, the zero set has efficiently verifiable certificates.

Based on joint ongoing work with S. Akshay, Aniket Muhrekar, Rohith Varma and Nikhil Vyas.

Joint Vérification/Automates seminar

Vérification

Lundi 17 juin 2019, 11 heures, Salle 3052

**Pierre-Malo Deniélou** (Google) *From MapReduce to Apache Beam: A Journey in Abstraction*

In this talk, I will present how the programming APIs (and underlying systems) for large-scale data processing evolved in the past 20 years, both within Google and in the open source world. I will start from MapReduce and Millwheel and finish with Apache Beam and where we're headed next.

(*) This will be a joint session of the Systèmes Complexes, Vérification and PPS seminars

Joint session of the Systèmes Complexes, Vérification and PPS seminars

Vérification

Mardi 11 juin 2019, 15 heures, Salle 3052

**Burcu Külahçıoğlu Özkan** (Max Planck Institute for Software Systems (MPI-SWS)) *Randomized Testing of Distributed Systems with Probabilistic Guarantees*

In this talk, we present a randomized scheduling algorithm for testing distributed systems. In contrast to previous approaches, our algorithm works for arbitrary partially ordered sets of events revealed online as the program is being executed. We show that for partial orders of width at most w and size at most n (both statically unknown), our algorithm is guaranteed to sample from at most w^2.n^(d−1) schedules, for every fixed bug depth d. Thus, our algorithm discovers a bug of depth d with probability at least 1/ (w^2.n^(d−1)). As a special case, our algorithm recovers a previous randomized testing algorithm for multithreaded programs. Our algorithm is simple to implement, but the correctness arguments depend on difficult combinatorial results about online dimension and online chain partitioning of partially ordered sets. In the last part of the talk, we briefly discuss how we can exploit state-space reduction strategies from model checking to provide better guarantees for the probability of hitting bugs. This will move us towards a randomized algorithm which brings together two orthogonal reductions of the search space: depth-bounded testing and dependency-aware testing.

(Joint work with Rupak Majumdar, Filip Niksic, Simin Oraee, Mitra Tabaei Befrouei, Georg Weissenbacher)

Vérification

Lundi 20 mai 2019, 11 heures, Salle 1007

**Raphaël Cauderlier** (Nomadic Labs) *Functional Verification of Tezos Smart Contracts in Coq*

The Tezos blockchain and its smart contract language Michelson have been designed with verification in mind. In this talk, I will present Mi-Cho-Coq, a formal specification of Michelson in the Coq proof assistant. I will also demonstrate how to use it for functional verification of a typical multisig smart contract.

Vérification

Vendredi 10 mai 2019, 11 heures, Salle 3052

**Mahsa Shirmohammadi** (LIS - CNRS & Univ. Aix-Marseille) *A Lesson on Timed Automata Reachability*

The old-standing, natural, and useful problem of characterizing the reachability relation for timed automata has been solved many times: by Hubert Comon and Yan Jurski, by Catalin Dima, by Pavol Krcal, etc. Still all these characterizations are difficult to understand and to use in practise. Recently, Mahsa Shirmohammadi and Ben Worrell came up with a new solution, anod moreover they say that it is very easy! Mahsa will present it in the form of a black-(or white-)board lesson on May 10th, from 11-13hs.

Abstract:

In our preprint (submitted to IPL)[*], we give a simple and short proof of effective definability of the reachability relation in timed automata. We use a small trick that reduces this problem to that of computing the set of configurations reachable from a fixed initial configuration in timed automata. The proof uses only Parikh theorem in heart and 1-bounded region automata, so to follow the proof one may not need any prior knowledge of timed automata.

This long seminar/lecture will run from 11hs to 13hs.

Vérification

Lundi 6 mai 2019, 11 heures, Salle 1007

**Matthieu Perrin** (Université de Nantes) *Shared Objects in Distributed Systems: A Broadcast Perspective*

To this end, it introduces a new broadcast communication abstraction, called k-SCD-Broadcast, which restricts the disagreement on the local deliveries of the messages that have been broadcast: 1-SCD-Broadcast boils down to total order broadcast and n-SCD-Broadcast is equivalent to the read/write register. Hence, in this context, k = 1 is not a special number, but only the first integer in an increasing integer sequence. This establishes a new “correspondence” between distributed agreement problems and communication abstractions, which enriches our understanding of the relations linking fundamental issues of fault-tolerant distributed computing.

Vérification

Mardi 16 avril 2019, 11 heures, Salle 3052

**Si Liu** (University of Illinois at Urbana-Champaign) *Design, Verification and Automatic Implementation of Correct-by-Construction Distributed Transaction Systems in Maude*

Vérification

Lundi 15 avril 2019, 11 heures, Salle 1007

**John Wickerson** (Imperial College London) *Using Alloy to explore Weak Memory and Transactional Memory*

This talk is about how we can formalise models of weak memory using a tool called Alloy. Using these formalisations, we can then synthesise programs that can distinguish different models of weak memory. We can also check whether a compiler mapping from one weak memory model to another is correct.

The main case study in this talk describes how we used Alloy to find problems in a prototype implementation of transaction memory being developed by ARM. I will also talk about how similar techniques can be used to check the correctness of software-to-hardware compilers (or “high-level synthesis” tools).

This talk is based on joint work with Mark Batty, Nathan Chong, George Constantinides, and Tyler Sorensen. For further reading, please see papers that appeared in [POPL'17](https://johnwickerson.github.io/papers/memalloy.pdf) and [PLDI'18](https://johnwickerson.github.io/papers/transactions.pdf).

Vérification

Jeudi 11 avril 2019, 14 heures, Salle 3052

**Ismail Kuru** (Drexel University) *Safe Deferred Memory Reclamation with Types*

Vérification

Vendredi 5 avril 2019, 14 heures 30, Salle 3052

**Cristoph Kirsch** (Universität Salzburg) *On the self in Selfie*

This is joint work with Alireza S. Abyaneh, Simon Bauer, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, and Manuel Widmoser, University of Salzburg, Austria

Web:

Vérification

Lundi 18 mars 2019, 11 heures, Salle 1007

**Glen Mével** (INRIA Paris) *Time Credits and Time Receipts in Iris*

Vérification

Vendredi 15 mars 2019, 11 heures, Salle 3052

**Sreeja Nair** (LIP 6 - Sorbonne Université) *Invariant safety for distributed applications*

In this talk, we present a proof methodology for verifying the safety of invariants of highly-available distributed applications that replicate state. The proof is modular and sequential :one can reason about each individual operation separately, and one can reason about a distributed application as if it were sequential. We automate the methodology and illustrate the use of the tool with a representative example.

Vérification

Lundi 11 mars 2019, 11 heures, Salle 1007

**Richard Bonichon** (CEA List) *Get rid of inline assembly through trustable verification-oriented lifting*

Vérification

Mardi 5 mars 2019, 11 heures, 3052

**Azadeh Farzan** (University of Toronto) *Automated Hypersafety Verification*

Vérification

Lundi 4 mars 2019, 11 heures, Salle 1007

**Marie Van Den Boogard** (Université Libre de Bruxelles) *Beyond admissibility: Dominance between chains of strategies*

Vérification

Lundi 25 février 2019, 11 heures, Salle 1007

**Pierre Courtieu** (CNAM) *A proof framework for mobile robots protocols*

We present a framework, named Pactole, for designing distributed protocols for mobile robots, stating properties about these protocols and proving these properties. We can also prove *impossibility statement* i.e. that there exists no protocol achieving some property.

Our technique cannot be compared to but can be seen as complementary to model checking in the sense that our proofs are not automated but allow for instance to conclude that a protocol is correct *for any* starting configuration, number of robots, that is not proven impossible.

Vérification

Lundi 25 février 2019, 11 heures, Salle 1007

**Corto Mascle** (ENS Paris-Saclay) *Non encore annoncé.*

Vérification

Lundi 18 février 2019, 14 heures, Salle 3052

**José Ignacio Requeno** (Université Grenoble Alpes) *Parameter Synthesis for Extended Signal Temporal Logic Specifications*

Vérification

Lundi 11 février 2019, 11 heures, Salle 1007

**Stéphane Demri** (LSV - CRNS & ENS Paris Saclay) *Modal Separation Logics and Friends*

Vérification

Lundi 28 janvier 2019, 11 heures, Salle 1007

**Mark Batty** (University of Kent) *A denotational semantics for weak-memory language concurrency with modular DRF-SC*

#### Année 2018

Vérification

Lundi 10 décembre 2018, 11 heures 10, Salle 1007

**Mahsa Shirmohammadi** (LIS - CNRS & Université Aix-Marseille) *On the Complexity of Value Iteration*

A preliminary draft of this work is available on arXiv:

Vérification

Lundi 3 décembre 2018, 11 heures 10, Salle 1007

**Vincent Rahli** (SnT - University of Luxembourg) *Building Reliable Systems on Reliable Foundations*

In this talk I will present some of my contributions to this area, namely, I will present my work on (1) designing formal verification tools to reason about complex distributed systems (such as Byzantine fault tolerant consensus protocols as used in Blockchain technology); and (2) on ensuring that those verification tools rely on correct foundations.

I will conclude by showing how I believe distributed systems will have a positive impact on modern foundational/logical frameworks, and vice versa.

Vérification

Lundi 26 novembre 2018, 11 heures 10, Salle 1007

**Matthias Függer** (LSV - CNRS & ENS de Cachan) *Fast Asymptotic and Approximate Consensus in Highly Dynamic Networks*

For many problems (distributed control, clock synchronization, load balancing, …) it is however sufficient to asymptotically converge to the same value, or decide on values not too far from each other. We study solvability of these consensus variants in highly dynamic networks, provide time complexity results, and present fast algorithms. We then show how the results on dynamic networks are relevant for classical fault-models, such as asynchronous message passing with crashes.

The talk is on previous and current research with Bernadette Charron-Bost (LIX), Thomas Nowak (LRI), and Manfred Schwarz (ECS, TU Wien).

Vérification

Lundi 12 novembre 2018, 11 heures 10, Salle 1007

**Arvid Jakobsson** (Huawei Research & LIFO -Université d'Orléans) *Replicated Synchronization of BSPlib Programs*

Vérification

Lundi 5 novembre 2018, 11 heures 10, Salle 1007

**Adrien Guatto** (IRIF) *Hierarchical Memory Management for Mutable State*

In this joint work with Sam Westrick, Ram Raghunathan, Umut Acar, and Matthew Fluet, we propose techniques for efficient mutation in parallel functional languages. To this end, we couple the memory manager with the thread scheduler to make reading and updating data allocated by nested threads efficient. We describe the key algorithms behind our technique, implement them in the MLton Standard ML compiler, and present an empirical evaluation. Our experiments show that the approach performs well, significantly improving efficiency over existing functional language implementations.

Vérification

Lundi 29 octobre 2018, 11 heures 10, Salle 1007

**Éric Tanter** (PLEIAD - Universidad de Chile & INRIA Paris) *The Essence of Gradual Typing*

Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. After a brief introduction to AGT, this talk reports on our experience applying AGT to various typing disciplines.

Vérification

Lundi 22 octobre 2018, 11 heures 10, Salle 1007

**Marie Fortin** (LSV - ENS Paris-Saclay) *It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with “Happened Before”*

This is joint work with Benedikt Bollig and Paul Gastin, presented at CONCUR’18.

Vérification

Lundi 1 octobre 2018, 11 heures 10, Salle 1007

**Mahsa Shirmohammadi** (LIS - CNRS & Université Aix-Marseille) *On Rationality of Nonnegative Matrix Factorization*

In this talk, we further exhibit a connection between Cohen and Rothblum's question with a question posed by Paz, in his seminal 1971 textbook. The latter question asks, given a probabilistic automaton (PA) with rational transition probabilities, does there always exist a minimal equivalent PA that also has rational transition probabilities? The PA and its minimal equivalent PA accept all finite words with equal probabilities. We use the established connection to answer Paz's question negatively, thus falsifying a positive answer claimed in 1974. (This talk is based on a paper in SODA 2017.)

Vérification

Lundi 24 septembre 2018, 11 heures 10, Salle 1007

**Adam Shimi** (IRIT - ENSEEIHT) *Characterizing Asynchronous Message-Passing Models Through Rounds*

I will present our formalization of this characterization for asynchronous models. Specifically, we introduce Delivered collections: the collection of all messages delivered at each round, whether late or not. Defining predicates on Delivered collections then allows us to capture message-passing models at the same level of abstraction than Heard-Of predicates. The question is then reformulated to: what Heard-Of predicates can be generated by a given Delivered predicate?

I will provide an answer by considering all possible scheduling of deliveries of messages from the Delivered collections and change of rounds for the processes. Strategies of processes then constrain those scheduling by specifying when processes can change rounds; those ensuring no process is ever blocked forever generate a Heard-Of collection per run, that is a Heard-Of predicate. Finally, we use these strategies to nd a characterizing Heard-Of predicate through a dominance relation on strategies: a dominant strategy for a Delivered predicate implements the most constrained Heard-Of predicate possible. This approach oer both the dominant Heard-Of predicates for classical asynchronous models and the existence, for every Delivered predicate, of a strategy dominating large classes of strategies. On the whole, those results confirm the power of this formalization and demonstrate the characterization of asynchronous models through rounds as a worthwhile pursuit.

This is joint work with Aurélie Hurault and Philippe Quéinnec.

Vérification

Lundi 17 septembre 2018, 11 heures, Salle 1007

**Franz Mayr** (Universidad ORT, Uruguay) *Regular inference on artificial neural networks*

Vérification

Vendredi 29 juin 2018, 11 heures, Salle 3052

**Mahsa Shirmohammadi** (LIS, CNRS - Univ. Aix-Marseille) *Costs and Rewards in Priced Timed Automata*

Vérification

Lundi 25 juin 2018, 11 heures, Salle 3052

**Nicolas Jeannerod** (IRIF) *Deciding the First-Order Theory of an Algebra of Feature Trees with Updates*

We plan to use feature trees as an abstract representation of file system tree transformations. We thus investigate an extension of these feature trees that includes the update operation, which expresses that two trees are similar except in a particular subtree where there might have been changes.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.

Vérification

Lundi 18 juin 2018, 11 heures, Salle 3052

**Eugène Asarin** (IRIF) *Distance on timed words and applications*

- it is global: it applies to words having different number of events;

- it is realistic and takes into account imprecise observation of timed events; thus it reflects the fact that the order of events cannot be observed whenever they are very close to each other;

- it is suitable for quantitative verification of timed systems: we formulate and solve quantitative model-checking and quantitative monitoring in terms of the new distance, with reasonable complexity;

- it is suitable for information-theoretical analysis of timed systems: due to its pre-compactness the quantity of information in bits per time unit can be correctly defined and computed.

(Joint work with Nicolas Basset and Aldric Degorre)

Vérification

Mercredi 13 juin 2018, 15 heures, Salle 3052

**Joël Ouaknine** (MPI-SWS) *Program Invariants*

This is joint work with Ehud Hrushovski, Amaury Pouly, and James Worrell.

Séminaire du Pôle ASV

Vérification

Lundi 11 juin 2018, 11 heures, Salle 3052

**François Pottier** (INRIA Paris) *Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic*

(This work was presented at CPP 2017.)

Vérification

Vendredi 1 juin 2018, 10 heures 30, 3052

**Derek Dreyer** (Max Planck Institute for Software Systems (MPI-SWS)) *RustBelt: Logical Foundations for the Future of Safe Systems Programming*

In this talk, I will present RustBelt (http://plv.mpi-sws.org/rustbelt), the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

After reviewing some essential features of the Rust language, I will describe the high-level structure of the RustBelt verification and then delve into detail about the secret weapon that makes RustBelt possible: the Iris framework for higher-order concurrent separation logic in Coq (http://iris-project.org). I will explain by example how Iris generalizes the expressive power of O'Hearn's original concurrent separation logic in ways that are essential for verifying the safety of Rust libraries. I will not assume any prior familiarity with concurrent separation logic or Rust.

This is joint work with Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and the rest of the Iris team.

Vérification

Lundi 28 mai 2018, 11 heures, Salle 1007

**Ana Sokolova** (Universität Salzburg, Austria) *Linearizability of Concurrent Data Structures via Order Extension Theorems*

In this talk, I will discuss the semantics of concurrent data structures and present recent order extension results (joint work with Harald Woracek) that lead to characterizations of linearizability in terms of violations, a.k.a. aspects. The approach works for pools, queues, and priority queues; finding other applications is ongoing work. In the case of pools and queues we obtain already known characterizations, but the proof method is new, elegant, and simple, and we expect that it will lead to deeper understanding of linearizability.

Vérification

Lundi 14 mai 2018, 11 heures, Salle 1007

**Raphaël Cauderlier** (IRIF - Université Paris Diderot) *A Verified Implementation of the Bounded List Container*

I will present a case study of full functional verification of the bounded doubly-linked list container of from the standard library of Ada 2012. This library is specified in SPARK and several client programs depend on this specification.

However, the low-level invariants required to verify this library cannot be expressed in SPARK. For this reason, the proof of functional correctness is done using VeriFast, a verification environment for Separation Logic extended with algebraic data types. The specifications proved entail the contracts of the Ada library and include new features. The verification method we used employs a precise algebraic model of the data structure and we show that it facilitates the verification and captures entirely the library contracts.

Vérification

Lundi 7 mai 2018, 11 heures, Salle 1007

**Adrien Pommellet** (IRIF) *Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous*

Vérification

Lundi 9 avril 2018, 11 heures, Salle 1007

**Ilya Sergey** (University College London, UK) *Programming and Proving with Distributed Protocols*

As a result, expensive verification efforts for key system components are not easily reusable, which hinders further verification efforts.

In my talk, I will present Disel, the first framework for implementation and reusable compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant.

In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel’s dependent type system, well-typed implementations always satisfy their protocols’ invariants and never go wrong, allowing users to verify system implementations interactively using Disel’s Hoare-style Separation Logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting.

KEYWORDS: Distributed Systems, Separation Logic, Dependent Types, Coq

Vérification

Lundi 26 mars 2018, 11 heures, Salle 1007

**Ivan Gazeau** (LORIA & INRIA Nancy - Grand Est) *Automated Verification of Privacy-type Properties for Security Protocols*

- a wide range of cryptographic primitives (in particular AKISS is the only tool able to verify equivalence properties for protocols that use xor);

- protocols with else branches (the treatment of disequalities is often complicated).

We will also provide some insights on how interleaving due to concurrency can be effectively handled.

Vérification

Vendredi 23 mars 2018, 14 heures 30, Salle 3052

**Javier Esparza** (Tecnhische Universität München) *One Theorem to Rule Them All: A Unified Translation of LTL into omega-Automata*

Joint work with Jan Kretinsky and Salomon Sickert.

Séminaire du Pôle: Automata, Structures, et Vérification

Vérification

Lundi 19 mars 2018, 11 heures, Salle 1007

**Rupak Majumdar** (Max Planck Institute for Software Systems (MPI-SWS)) *Effective Random Testing for Concurrent and Distributed Programs*

Vérification

Lundi 12 mars 2018, 11 heures, Salle 1007

**Thomas Colcombet** (IRIF & CNRS) *Automata and Program Analysis*

Vérification

Lundi 26 février 2018, 11 heures, Salle 1007

**Cătălin Hriţcu** (INRIA Paris) *When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise*

To illustrate this model, we build a secure compilation chain for an unsafe language with buffers, procedures, and components. We compile it to a simple RISC abstract machine with built-in compartmentalization and provide thorough proofs, many of them machine-checked in Coq, showing that the compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor.

Vérification

Lundi 19 février 2018, 11 heures, Salle 3052

**Adrien Boiret** (University of Warsaw) *The “Hilbert Method” for Solving Transducer Equivalence Problems.*

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

-We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.

-We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

Joint Session w/ the ACS working group

Vérification

Jeudi 8 février 2018, 10 heures 30, Salle 3052

**Vincent Laporte** (IMDEA Software) *Provably secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”*

We consider the problem of preserving side-channel countermeasures by compilation for cryptographic “constant-time”, a popular countermeasure against cache-based timing attacks. We present a general method, based on the notion of 2-simulation, for proving that a compilation pass preserves the constant-time countermeasure. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

(Joint session with the PPS seminar)

Vérification

Lundi 29 janvier 2018, 11 heures, Salle 1007

**Engel Lefaucheaux** (ENS Cachan / IRISA Rennes) *Probabilistic Disclosure: Maximisation vs. Minimisation*

Vérification

Lundi 22 janvier 2018, 11 heures, Salle 1007

**Josef Widder** (TU Wien) *Synthesis of Distributed Algorithms with Parameterized Thresholds Guards*

This is joint work with Marijana Lazić, Igor Konnov, and Roderick Bloem.

Vérification

Lundi 15 janvier 2018, 11 heures, Salle 1007

**Chao Wang** (IRIF) *Checking Linearizability of Concurrent Priority Queues*

Vérification

Lundi 8 janvier 2018, 11 heures, Salle 1007

**Jean-Jacques Lévy** (IRIF & INRIA) *Proofs of graph algorithms with automation and their readability*

This is joint work with Ran Chen and was presented at VSTTE 2017. The Coq and Isabelle proofs were achieved by Cyril Cohen, Laurent Théry and Stephan Merz.

#### Année 2017

Vérification

Lundi 11 décembre 2017, 11 heures, Salle 1007

**Irène Guessarian** (IRIF - Unviersité Paris Diderot) *Congruence Preservation, Lattices and Recognizability*

Vérification

Jeudi 7 décembre 2017, 16 heures, Salle 1007

**Luke Ong** (University of Oxford) *Constrained Horn clauses for automatic program verification: the higher-order case*

Vérification

Mardi 28 novembre 2017, 13 heures 30, Salle 3052

**Léon Gondelman** (Radboud University, The Netherlands) *The Spirit of Ghost Code*

The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Joint session with the ACS Work group

Vérification

Lundi 20 novembre 2017, 11 heures, Salle 1007

**Laurent Fribourg** (LSV, CNRS & ENS de Cachan) *Euler’s Method Applied to the Control of Switched Systems*

We will sketch out how the approach relates with other symbolic methods based on interval arithmetic and Lyapunov functions. We will also present some applicative examples which illustrate its advantages and limitations.

Vérification

Lundi 13 novembre 2017, 11 heures, Salle 1007

**Viktor Vafeiadis** (Max Planck Institute for Software Systems (MPI-SWS)) *Effective Stateless Model Checking for C/C++ Concurrency*

(This is joint work with Michalis Kokologiannakis, Ori Lahav, and Konstantinos Sagonas, and will appear at POPL'18.)

Vérification

Lundi 30 octobre 2017, 11 heures, Salle 1007

**Suha Mutluergil** (Koç University) *Proving linearizability using forward simulations*

Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy & Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to simple and natural correctness proofs for these implementations that are amenable to automation.

Vérification

Lundi 23 octobre 2017, 11 heures, Salle 1007

**Raphaël Cauderlier** (IRIF - Université Paris Diderot) *FocaLiZe and Dedukti to the Rescue for Proof Interoperability*

Vérification

Lundi 16 octobre 2017, 11 heures, Salle 1007

**Noam Rineztky** (Tel-Aviv University) *Verifying Equivalence of Spark Programs*

In this paper, we present a novel SMT-based technique for verifying the equivalence of Spark programs. We model Spark as a programming language whose semantics imitates Relational Algebra queries (with aggregations) over bags (multisets) and allows for UDFs expressible in Presburger Arithmetics. We prove that the problem of checking equivalence is undecidable even for programs which use a single aggregation operator. Thus, we present sound techniques for verifying the equivalence of interesting classes of Spark programs, and show that it is complete under certain restrictions. We implemented our technique, and applied it to a few small, but intricate, test cases.

Joint work with: Shelly Grossman, Sara Cohen, Shachar Itzhaky, and Mooly Sagiv Presented in CAV’17

Vérification

Lundi 9 octobre 2017, 11 heures, Salle 1007

**Javier Esparza** (Technische Universität München) *Polynomial Analysis Algorithms for Free-Choice Workflow Nets*

While the state space of a free-choice net can grow exponentially in its number of nodes, numerous control-flow properties can still be decided in polynomial time. However, these decision algorithms cannot be extended to workflow nets with data. We present a new analysis technique, based on reduction rules, that can be applied to workflow nets with data, costs, or probabilities. In particular, we give a polynomial algorithm to compute the expected cost of sound free-choice workflow nets.

Vérification

Lundi 2 octobre 2017, 11 heures, Salle 1007

**Ahmed Bouajjani** (IRIF - Université Paris Diderot) *Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency*

Joint work with Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran.

Vérification

Mercredi 28 juin 2017, 14 heures, Salle 3052

**Giuliano Losa** (UCLA) *Paxos Made EPR — Decidable Reasoning about Distributed Consensus*

This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Sch\“onfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos and Flexible Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos and Fast Paxos.

This is joint work with O. Padon, M. Sagiv, and S. Shoham.

Vérification

Jeudi 22 juin 2017, 11 heures, Salle 3052

**Ruzica Piskac** (Yale University) *New Applications of Software Synthesis: Verification of Configuration Files and Firewalls Repair*

We also outline a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls - whether the policies in the firewalls meet the specifications of their administrators - is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.

Vérification

Lundi 12 juin 2017, 14 heures, Salle 3052

**Thomas Wies** (New York University) *A Simple Framework for Verifying Concurrent Search Structures*

Vérification

Mardi 6 juin 2017, 11 heures, Salle 3052

**Sergio Rajsbaum** (UNAM Mexico) *Tasks, objects, and the notion of a distributed problem*

In distributed computing tasks have been studied from early on, in parallel, but independently of \emph{sequential objects}. While tasks explicitly state what might happen when a set of processes run concurrently, sequential objects only specify what happens when processes run sequentially. Indeed, many distributed problems considered in the literature, seem to have no natural specification neither as tasks nor as sequential objects. I will concentrate on our recent work on interval-linearizability, a notion we introduced to specify objects more general than the usual sequential objects. I will describe the bridges we establish between these two classical paradigms, and our discussions about what is a distributed problem, and what it means to solve it.

Vérification

Jeudi 1 juin 2017, 11 heures, Salle 3052

**Orna Grumberg** (Technion, Israel) *Sound and Complete Mutation-Based Program Repair*

We impose no assumptions on the number of erroneous locations in the program, yet we are able to guarantee soundness and completeness. That is, we assure that a program is returned iff it is minimal and bounded correct.

Searching the space of mutated programs is reduced to searching unsatisfiable sets of constraints, which is performed efficiently using a sophisticated cooperation between SAT and SMT solvers. Similarities between mutated programs are exploited in a new way, by using both the SAT and the SMT solvers incrementally.

We implemented a prototype of our algorithm, compared it with a state-of-the-art repair tool and got very encouraging results. This is a joint work with Bat-Chen Rothenberg.

Vérification

Mardi 23 mai 2017, 15 heures 30, Salle 3052

**Florian Zuleger** (TU Wien) *Inductive Termination Proofs by Transition Predicate Abstraction and their relationship to the Size-Change Abstraction*

Vérification

Lundi 22 mai 2017, 11 heures, Salle 1007

**Alain Finkel** (LSV, ENS Cachan) *The Erdös & Tarski theorem. A new class of WSTS without WQO.*

Vérification

Lundi 27 mars 2017, 11 heures, Salle 1007

**Mohamed Faouzi Atig** (Uppsala University) *Lossy Channel Systems with Data.*

In the second part of the talk, we extend lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

This talk is based on previous joint work with Parosh Aziz Abdula, Jonathan Cederberg and C. Aiswarya.

Vérification

Lundi 20 mars 2017, 11 heures, Salle 1007

**Andreas Podelski** (University of Freiburg) *Proving Liveness of Parameterized Programs*

Vérification

Lundi 13 mars 2017, 11 heures, Salle 1007

**Ori Lahav** (MPI Kaiserslautern) *A Promising Semantics for Relaxed-Memory Concurrency*

Joint work with Jeehoon Kang, Chung-Kil Hur, Viktor Vafeiadis, and Derek Dreyer, recently presented at POPL'17

Vérification

Lundi 6 mars 2017, 11 heures, Salle 1007

**Germán Andrés Delbianco** (IMDEA Madrid) *Concurrent Data Structures Linked in Time*

In this talk I will present a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs.

We have named the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. In order to illustrate our approach, I will illustrate its application to verify (mechanically in Coq) an intricate optimal snapshot algorithm, due to Jayanti.

Vérification

Lundi 27 février 2017, 11 heures, Salle 1007

**Oded Maler** (CNRS and University of Grenoble-Alpes) *Monitoring: Qualitative and Quantitative, Real and Virtual, Online and Offline*

Vérification

Lundi 20 février 2017, 11 heures, Salle 1007

**Loig Jezequel** (L2SN - Nantes) *Lazy Reachability Analysis in Distributed Systems*

Vérification

Lundi 23 janvier 2017, 11 heures, Salle 1007

**Andrea Cerone** (Imperial College London) *Analysing Snapshot Isolation*

#### Année 2016

Vérification

Lundi 12 décembre 2016, 11 heures, Salle 1007

**Bin Fang** (IRIF(Paris), ECNU (China)) *Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators (a logic-based approach)*

Vérification

Vendredi 9 décembre 2016, 11 heures, Salle 3052

**Alastair Donaldson** (Imperial College London) *Exposing Errors Related to Weak Memory in GPU Applications*

Vérification

Lundi 5 décembre 2016, 11 heures, Salle 1007

**Guilhem Jaber** (IRIF) *SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence*

Vérification

Lundi 28 novembre 2016, 11 heures, Salle 1007

**Georg Zetzsche** (LSV, ENS Cachan) *First-order logic with reachability for infinite-state systems*

This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FOR is decidable for the resulting transition systems.

Vérification

Jeudi 24 novembre 2016, 15 heures, Salle 3052

**Gennaro Parlato** (University of Southampton) *A Pragmatic Bug-finding Approach for Concurrent Programs*

Vérification

Lundi 14 novembre 2016, 11 heures, Salle 1007

**Philipp Rümmer** (University of Uppsala) *Liveness of Randomised Parameterised Systems under Arbitrary Schedulers*

Joint work with Anthony W. Lin.

Vérification

Lundi 24 octobre 2016, 11 heures, Salle 1007

**Sylvain Schmitz** (LSV - ENS Cachan) *Ideal Decompositions for Vector Addition Systems*

Joint work with Jérôme Leroux.

Vérification

Lundi 10 octobre 2016, 11 heures, Salle 1007

**Steven de Oliveira** (CEA) *Polynomial invariants by linear algebra*

I will present in this talk a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces a class of loops containing polynomial assignments to linear loops and a procedure for generating inductive invariants for linear loops.

Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification as a Frama-C plug-in, PILAT.

Vérification

Lundi 3 octobre 2016, 11 heures, Salle 1007

**Giovanni Bernardi** (IRIF) *Robustness against Consistency Models with Atomic Visibility*

Vérification

Lundi 26 septembre 2016, 11 heures, Salle 1007

**Arnaud Sangnier** (IRIF) *Fixpoints in VASS: Results and Applications*

Vérification

Lundi 19 septembre 2016, 11 heures, Salle 1007

**Francesco Belardinelli** (Université d'Evry) *Abstraction-based Verification of Infinite-state Data-aware Systems*

DaS are best described in terms of interacting modules consisting of a data model and a lifecycle, which account respectively for the relational structure of data and their evolution over time.

However, by considering data and processes as equally relevant tenets of DaS, the typical questions concerning their verification are hardly amenable by current methodologies. For instance, the presence of data means that the number of states in DaS is infinite in general.

In this talk we present recent advances in the verification of DaS. We introduce agent-based abstraction techniques to model check DaS against specifications expressed in temporal and strategy logics. Further, we illustrate how DaS can be useful to model game-theoretic scenarios as well. Specifically, we provide an analysis of English (ascending bid) auctions through DaS.

Vérification

Lundi 30 mai 2016, 11 heures, Salle 1007

**Thibaut Balabonski** (LRI) *Low-level C code optimisations: are they valid?*

Vérification

Lundi 14 mars 2016, 11 heures, Salle 1007

**Paul Gastin** (LSV) *Formal methods for the verification of distributed algorithms*

Vérification

Lundi 7 mars 2016, 11 heures, Salle 1007

**Julien Signoles** (CEA-LIST) *Frama-C, a collaborative and extensible framework for C code analysis*

Vérification

Lundi 29 février 2016, 11 heures, Salle 1007

**Pierre Fraigniaud** (IRIF) *Fault-Tolerant Decentralized Runtime Monitoring*