## Verification

#### Day, hour and place

Monday at 11:00am, room 1007

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

### Previous talks

#### Year 2024

Verification

Monday June 17, 2024, 11AM, 4071 and Zoom link

**Shibashis Guha** (TIFR Mumbai) *Strategy synthesis for global window PCTL*

Joint work with Benjamin Bordais, Damien Busatto-Gaston, and Jean-François Raskin

Verification

Monday May 27, 2024, 11AM, 3052 and Zoom link

**Nicolas Amat** (IMDEA) *A polyhedral Framework for Reachability Problems in Petri Nets*

The correctness of this method is based on a new notion of equivalence between nets. Combined with an SMT-based model checker, one can transform a reachability problem about some Petri net, into the verification of an equivalent reachability property on a reduced version of this net. We also propose an automated procedure to prove that such an abstraction is correct, exploiting a connection with a class of Petri nets with Presburger-definable reachability sets.

In addition, we present a data structure, called Token Flow Graph (TFG), that captures the particular structure of constraints stemming from structural reductions. We leverage TFGs to efficiently solve two problems. First, to eliminate quantifiers that appear during our transformation, in the updated formula to be checked on the reduced net. Second, to compute the concurrency relation of a net, that is all pairs of places that can be marked simultaneously in some reachable marking.

We apply our approach to several symbolic model checking procedures and introduce a new semi-decision procedure for checking reachability properties in Petri nets based on the Property Directed Reachability (PDR) method. A distinctive feature of this PDR method is its ability to generate verdict certificates that can be verified using an external SMT solver.

Our approach and algorithms are implemented in four open-source tools: SMPT for checking reachability properties; Kong for accelerating the computation of concurrent places; Octant for eliminating quantifiers; and Reductron for automatically proving the correctness of polyhedral reductions. We give experimental results about their effectiveness, both for bounded and unbounded nets, using a large benchmark provided by the Model Checking Contest.

Verification

Monday May 13, 2024, 11AM, 3052 and Zoom link

**Enrique Román Calvo** (IRIF) *Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels*

In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.

Verification

Monday May 6, 2024, 11AM, 3052 and Zoom link

**Giovanni Bernardi** (IRIF) *Constructive characterisations of the must-preorder for asynchrony*

I will outline the first characterisations of the must-preorder that are constructive, supported by a mechanisation in Coq, and independent from any calculus: the results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate asynchronously via a shared unordered buffer, as in asynchronous CCS or the asynchronous π-calculus.

The results are surprising: the behavioural characterisations devised for synchronous communication carry over as they stand to the asynchronous setting, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer.

Verification

Monday April 29, 2024, 11AM, 3052 and Zoom link

**Niklas Kochdumper** (IRIF) *Neural Network Verification using Polynomial Zonotopes*

Verification

Monday April 22, 2024, 11AM, 3052 (streamed) and Zoom link

**Sidi Mohamed Beillahi** (University of Toronto) *Securing Smart Contracts Through Program Synthesis*

In this talk, I will first present a work on automated synthesis of adversarial transactions that exploit DeFi smart contracts using flash loans. To bypass the complexity of a DeFi protocol and needs for source code analysis, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack that is constituted of a sequence of functions invocations with optimal parameters that provides the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique.

I will then present a followup work studying a category of DeFi attacks known as oracle manipulation attacks and the effectiveness of the current mechanisms used to protect against those attacks. I will show that those mechanisms are inadequate to ensure DeFi smart contracts safety when confronted with significant oracle deviations. I will then present a new framework to identify parameters that allow to secure DeFi smart contracts against oracle manipulation attacks. In the framework, we first perform symbolic analysis on the given contract and construct a summary model of constraints. We then leverage an SMT solver to identify parameters values that allow to secure smart contracts against oracle deviations.

The talk is based on two ICSE 2024 papers that are joint works with Zhiyang Chen, Xun Deng, Andreas Veneris, and Fan Long (University of Toronto) and Cyrus Minwalla and Han Du (Bank of Canada).

Verification

Monday March 25, 2024, 11AM, 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).

Verification

Monday March 18, 2024, 11AM, 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.

Verification

Monday March 11, 2024, 11AM, 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

Verification

Monday March 4, 2024, 11AM, 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

Verification

Monday February 26, 2024, 11AM, 3052 and Zoom link

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

Verification

Monday February 19, 2024, 11AM, 3052 and Zoom link

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

Verification

Monday February 12, 2024, 11AM, 3052 and Zoom link

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

Verification

Monday February 5, 2024, 11AM, Zoom link

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

Verification

Monday January 15, 2024, 11AM, 3052 and Zoom link

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

Verification

Monday January 8, 2024, 11AM, 3052 and Zoom link

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

#### Year 2023

Verification

Monday December 18, 2023, 11AM, 3052 and Zoom link

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

Verification

Monday December 4, 2023, 11AM, 3052 and Zoom link

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

Verification

Monday November 20, 2023, 11AM, Zoom link

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

Verification

Monday November 6, 2023, 11AM, 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

Verification

Monday October 16, 2023, 11AM, 3052 and Zoom link

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

Verification

Monday October 9, 2023, 11AM, 3052 and Zoom link

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

Verification

Monday September 25, 2023, 11AM, 3052 and Zoom link

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

Verification

Monday June 26, 2023, 11AM, Olympe de Gouges 146 and Zoom link

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

Verification

Monday June 19, 2023, 11AM, Olympe de Gouges 146 and Zoom link

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

Verification

Monday June 12, 2023, 11AM, 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.

Verification

Monday June 5, 2023, 11AM, Olympe de Gouges 146 and Zoom link

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

Verification

Monday May 22, 2023, 11AM, 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.

Verification

Monday May 15, 2023, 11AM, Olympe de Gouges 146 and Zoom link

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

Verification

Tuesday May 9, 2023, 2PM, 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*

Verification

Monday April 17, 2023, 11AM, 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.

Verification

Monday April 3, 2023, 11AM, 1007 and Zoom link

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

Verification

Monday March 27, 2023, 11AM, 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.

Verification

Monday March 20, 2023, 11AM, 1007 and Zoom link

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

Verification

Monday March 13, 2023, 11AM, 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.

Verification

Monday March 6, 2023, 11AM, 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.

Verification

Monday February 20, 2023, 11AM, 1007 and Zoom link

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

Verification

Monday February 13, 2023, 11AM, 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.

Verification

Monday February 6, 2023, 11AM, 1007 and Zoom link

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

Verification

Monday January 30, 2023, 11AM, 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.

Verification

Monday January 30, 2023, 11AM, 3052 and Zoom link

**Sarah Winter** (IRIF) *To be announced.*

Verification

Monday January 23, 2023, 11AM, 1007 and Zoom link

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

Online seminar streamed in room 1007.

Verification

Monday January 16, 2023, 11AM, 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.

Verification

Monday January 9, 2023, 11AM, 1007 and Zoom link

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

Online seminar streamed in room 1007.

#### Year 2022

Verification

Monday December 12, 2022, 11AM, 1007 and Zoom link

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

Verification

Monday December 5, 2022, 11AM, 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.

Verification

Monday November 28, 2022, 11AM, 1007 and Zoom link

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

Verification

Monday November 21, 2022, 11AM, 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.

Verification

Monday November 14, 2022, 11AM, 1007 and Zoom link

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

Verification

Monday November 7, 2022, 11AM, 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.

Verification

Monday October 24, 2022, 11AM, 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.

Verification

Tuesday October 18, 2022, 4PM, 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.

Verification

Monday October 10, 2022, 11AM, 3052 and Zoom link

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

Verification

Monday September 19, 2022, 11AM, 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.

Verification

Monday July 11, 2022, 11AM, 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.

Verification

Monday July 4, 2022, 11AM, 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.

Verification

Monday June 27, 2022, 11AM, 3052 and Zoom link

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

Verification

Monday June 20, 2022, 11AM, 3052 and Zoom link

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

Verification

Monday May 30, 2022, 11AM, 3052 and Zoom link

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

Verification

Monday May 16, 2022, 11AM, 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>.

Verification

Monday May 9, 2022, 11AM, 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.

Verification

Monday April 11, 2022, 11AM, 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.

Verification

Monday March 28, 2022, 11AM, 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.

Verification

Monday March 14, 2022, 11AM, Zoom link

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

Verification

Monday March 7, 2022, 11AM, 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.

Verification

Monday February 28, 2022, 11AM, 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*

Verification

Monday January 31, 2022, 11AM, Zoom link

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

#### Year 2021

Verification

Monday December 13, 2021, 11AM, Zoom link

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

Verification

Monday December 6, 2021, 11AM, 1007 and Zoom link

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

Verification

Monday November 22, 2021, 11AM, 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.

Verification

Monday October 18, 2021, 11AM, 3052 and Zoom link

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

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

Verification

Monday September 27, 2021, 11AM, 1007 and Zoom link

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

Verification

Monday September 13, 2021, 11AM, 3052 and BBB link

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

Verification

Monday July 5, 2021, 11AM, 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.

Verification

Monday June 28, 2021, 11AM, BBB link

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

Verification

Monday June 14, 2021, 11AM, 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.

Verification

Monday June 7, 2021, 11AM, 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.

Verification

Monday May 17, 2021, 11AM, BBB link

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

This a joint work with Ahmed Bouajjani and Constantin Enea.

Verification

Monday May 10, 2021, 11AM, 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.

Verification

Monday April 12, 2021, 11AM, 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.

Verification

Monday March 22, 2021, 11AM, BBB link

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

Verification

Monday March 15, 2021, 11AM, BBB link

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

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

Verification

Monday March 1, 2021, 11AM, BBB link

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

Verification

Thursday February 25, 2021, 4PM, 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).

Verification

Monday February 22, 2021, 11AM, BBB link

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

Verification

Monday February 15, 2021, 11AM, BBB link

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

Verification

Monday February 8, 2021, 11AM, 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.

Verification

Monday February 1, 2021, 11AM, BBB link

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

Verification

Monday January 18, 2021, 11AM, BBB link

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

Verification

Monday January 11, 2021, 11AM, BBB link

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

#### Year 2020

Verification

Monday December 14, 2020, 11AM, 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.

Verification

Monday December 7, 2020, 11AM, BBB link

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

Verification

Monday November 30, 2020, 11AM, BBB link

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

Verification

Monday November 23, 2020, 11AM, BBB link

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

Verification

Monday November 16, 2020, 11AM, 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).

Verification

Monday November 9, 2020, 11AM, 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

Verification

Monday November 2, 2020, 11AM, BBB link

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

Verification

Monday October 19, 2020, 11AM, BBB link

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

LICS 2020 paper

Verification

Monday July 13, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Monday July 6, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Monday June 29, 2020, 11AM, (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.

Verification

Monday June 22, 2020, 11AM, (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.

Verification

Monday June 15, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Monday June 8, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Wednesday June 3, 2020, 2PM, (online, using BigBlueButton)

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

Verification

Monday May 25, 2020, 11AM, (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.

Verification

Monday May 18, 2020, 11AM, (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.

Verification

Monday May 11, 2020, 11AM, (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/

Verification

Monday May 4, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Monday April 27, 2020, 11AM, (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.

Verification

Monday April 20, 2020, 11AM, (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.

Verification

Wednesday April 15, 2020, 3PM, (online, using BigBlueButton)

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

Verification

Monday April 6, 2020, 11AM, (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.

Verification

Monday March 30, 2020, 11AM, (online, using BigBlueButton)

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

Verification

Monday March 30, 2020, 11AM, Salle 1007

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

Verification

Monday March 16, 2020, 11AM, Salle 1007

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

Verification

Monday March 9, 2020, 11AM, Salle 1007

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

Verification

Monday March 2, 2020, 11AM, Salle 1007

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

Verification

Monday February 24, 2020, 11AM, Salle 1007

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

Verification

Monday February 17, 2020, 11AM, Salle 1007

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

Verification

Monday February 10, 2020, 11AM, 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.

Verification

Friday January 10, 2020, 10AM, 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.

#### Year 2019

Verification

Monday December 16, 2019, 11AM, 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.

Verification

Wednesday December 11, 2019, 11AM, 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.

Verification

Monday December 9, 2019, 11AM, 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.

Verification

Friday November 29, 2019, 2:30PM, 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).

Verification

Friday November 29, 2019, 11AM, Salle 3052

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

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

Verification

Monday November 18, 2019, 11AM, Salle 1007

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

Verification

Friday November 15, 2019, 2:30PM, 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.

Verification

Monday November 4, 2019, 11AM, Salle 1007

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

Verification

Monday October 28, 2019, 11AM, Salle 1007

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

Verification

Monday October 21, 2019, 11AM, Salle 1007

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

Verification

Monday October 14, 2019, 11AM, 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.

Verification

Monday September 23, 2019, 11AM, Salle 1007

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

Verification

Friday July 5, 2019, 2:30PM, Salle 1001

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

Joint Automata & Verification Seminars

Verification

Monday July 1, 2019, 2PM, 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

Verification

Monday June 17, 2019, 11AM, 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

Verification

Tuesday June 11, 2019, 3PM, 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)

Verification

Monday May 20, 2019, 11AM, 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.

Verification

Friday May 10, 2019, 11AM, 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.

Verification

Monday May 6, 2019, 11AM, 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.

Verification

Tuesday April 16, 2019, 11AM, Salle 3052

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

Verification

Monday April 15, 2019, 11AM, 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).

Verification

Thursday April 11, 2019, 2PM, Salle 3052

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

Verification

Friday April 5, 2019, 2:30PM, 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:

Verification

Monday March 18, 2019, 11AM, Salle 1007

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

Verification

Friday March 15, 2019, 11AM, 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.

Verification

Monday March 11, 2019, 11AM, Salle 1007

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

Verification

Tuesday March 5, 2019, 11AM, 3052

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

Verification

Monday March 4, 2019, 11AM, Salle 1007

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

Verification

Monday February 25, 2019, 11AM, 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.

Verification

Monday February 25, 2019, 11AM, Salle 1007

**Corto Mascle** (ENS Paris-Saclay) *To be announced.*

Verification

Monday February 18, 2019, 2PM, Salle 3052

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

Verification

Monday February 11, 2019, 11AM, Salle 1007

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

Verification

Monday January 28, 2019, 11AM, Salle 1007

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

#### Year 2018

Verification

Monday December 10, 2018, 11:10AM, 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:

Verification

Monday December 3, 2018, 11:10AM, 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.

Verification

Monday November 26, 2018, 11:10AM, 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).

Verification

Monday November 12, 2018, 11:10AM, Salle 1007

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

Verification

Monday November 5, 2018, 11:10AM, 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.

Verification

Monday October 29, 2018, 11:10AM, 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.

Verification

Monday October 22, 2018, 11:10AM, 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.

Verification

Monday October 1, 2018, 11:10AM, 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.)

Verification

Monday September 24, 2018, 11:10AM, 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.

Verification

Monday September 17, 2018, 11AM, Salle 1007

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

Verification

Friday June 29, 2018, 11AM, Salle 3052

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

Verification

Monday June 25, 2018, 11AM, 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.

Verification

Monday June 18, 2018, 11AM, 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)

Verification

Wednesday June 13, 2018, 3PM, 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

Verification

Monday June 11, 2018, 11AM, 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.)

Verification

Friday June 1, 2018, 10:30AM, 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.

Verification

Monday May 28, 2018, 11AM, 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.

Verification

Monday May 14, 2018, 11AM, 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.

Verification

Monday May 7, 2018, 11AM, Salle 1007

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

Verification

Monday April 9, 2018, 11AM, 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

Verification

Monday March 26, 2018, 11AM, 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.

Verification

Friday March 23, 2018, 2:30PM, 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

Verification

Monday March 19, 2018, 11AM, Salle 1007

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

Verification

Monday March 12, 2018, 11AM, Salle 1007

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

Verification

Monday February 26, 2018, 11AM, 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.

Verification

Monday February 19, 2018, 11AM, 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

Verification

Thursday February 8, 2018, 10:30AM, 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)

Verification

Monday January 29, 2018, 11AM, Salle 1007

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

Verification

Monday January 22, 2018, 11AM, 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.

Verification

Monday January 15, 2018, 11AM, Salle 1007

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

Verification

Monday January 8, 2018, 11AM, 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.

#### Year 2017

Verification

Monday December 11, 2017, 11AM, Salle 1007

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

Verification

Thursday December 7, 2017, 4PM, Salle 1007

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

Verification

Tuesday November 28, 2017, 1:30PM, 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

Verification

Monday November 20, 2017, 11AM, 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.

Verification

Monday November 13, 2017, 11AM, 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.)

Verification

Monday October 30, 2017, 11AM, 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.

Verification

Monday October 23, 2017, 11AM, Salle 1007

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

Verification

Monday October 16, 2017, 11AM, 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

Verification

Monday October 9, 2017, 11AM, 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.

Verification

Monday October 2, 2017, 11AM, 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.

Verification

Wednesday June 28, 2017, 2PM, 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.

Verification

Thursday June 22, 2017, 11AM, 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.

Verification

Monday June 12, 2017, 2PM, Salle 3052

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

Verification

Tuesday June 6, 2017, 11AM, 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.

Verification

Thursday June 1, 2017, 11AM, 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.

Verification

Tuesday May 23, 2017, 3:30PM, Salle 3052

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

Verification

Monday May 22, 2017, 11AM, Salle 1007

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

Verification

Monday March 27, 2017, 11AM, 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.

Verification

Monday March 20, 2017, 11AM, Salle 1007

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

Verification

Monday March 13, 2017, 11AM, 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

Verification

Monday March 6, 2017, 11AM, 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.

Verification

Monday February 27, 2017, 11AM, Salle 1007

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

Verification

Monday February 20, 2017, 11AM, Salle 1007

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

Verification

Monday January 23, 2017, 11AM, Salle 1007

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

#### Year 2016

Verification

Monday December 12, 2016, 11AM, Salle 1007

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

Verification

Friday December 9, 2016, 11AM, Salle 3052

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

Verification

Monday December 5, 2016, 11AM, Salle 1007

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

Verification

Monday November 28, 2016, 11AM, 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.

Verification

Thursday November 24, 2016, 3PM, Salle 3052

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

Verification

Monday November 14, 2016, 11AM, Salle 1007

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

Joint work with Anthony W. Lin.

Verification

Monday October 24, 2016, 11AM, Salle 1007

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

Joint work with Jérôme Leroux.

Verification

Monday October 10, 2016, 11AM, 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.

Verification

Monday October 3, 2016, 11AM, Salle 1007

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

Verification

Monday September 26, 2016, 11AM, Salle 1007

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

Verification

Monday September 19, 2016, 11AM, 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.

Verification

Monday May 30, 2016, 11AM, Salle 1007

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

Verification

Monday March 14, 2016, 11AM, Salle 1007

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

Verification

Monday March 7, 2016, 11AM, Salle 1007

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

Verification

Monday February 29, 2016, 11AM, Salle 1007

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