## 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 given this link

#### Contact(s)

### Next talks

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

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 24, 2020, 11AM, Salle 1007

**James Worrell** (University of Oxford) *To be announced.*

Verification

Monday March 2, 2020, 11AM, Salle 1007

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

Verification

Monday March 9, 2020, 11AM, Salle 1007

**Nathan Thomasset** (ENS de Rennes.) *To be announced.*

Verification

Monday March 16, 2020, 11AM, Salle 1007

**Matteo Mio** (CNRS & ENS de Lyon) *To be announced.*

Verification

Monday May 4, 2020, 11AM, Salle 1007

**Dumitru Potop-Butucaru** (INRIA Paris) *To be announced.*

Verification

Monday May 11, 2020, 11AM, Salle 1007

**Viktor Kuncak** (EPFL) *To be announced.*

### Previous talks

#### Year 2020

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*