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
Friday November 29, 2019, 2:30PM, Salle 3052
Dmitry Chistikov (University of Warwick) On the complexity of linear arithmetic theories over the integers

Given a system of linear Diophantine equations, how difficult is it to determine whether it has a solution? What changes if equations are replaced with inequalities? If some of the variables are quantified universally? These and similar questions relate to the computational complexity of deciding the truth value of statements in various logics. This includes in particular Presburger arithmetic, the first-order logic over the integers with addition and order.

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
Monday December 2, 2019, 11AM, Salle 1007
Sidi Mohamed Beillahi (IRIF) Checking Robustness Against Snapshot Isolation

Transactional access to databases is an important abstraction allowing programmers to consider blocks of actions (transactions) as executing in isolation. The strongest consistency model is serializability, which ensures the atomicity abstraction of transactions executing over a sequentially consistent memory. Since ensuring serializability carries a significant penalty on availability, modern databases provide weaker consistency models, one of the most prominent being snapshot isolation. In general, the correctness of a program relying on serializable transactions may be broken when using weaker models. However, certain programs may also be insensitive to consistency relaxations, i.e., all their properties holding under serializability are preserved even when they are executed over a weak consistent database and without additional synchronization.

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
Monday December 9, 2019, 11AM, Salle 1007
Corto Mascle (ENS Paris-Saclay) To be announced.

Verification
Monday December 16, 2019, 11AM, Salle 1007
Jules Villard (Facebook) To be announced.


Previous talks



Year 2019

Verification
Monday November 18, 2019, 11AM, Salle 1007
Arnaud Sangnier (IRIF) The Complexity of Flat Freeze LTL

We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.

Verification
Friday November 15, 2019, 2:30PM, Salle 3052
Patrick Totzke (Liverpool University) Timed Basic Parallel Processes

I will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential Linear Arithmetic.

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

A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, the use of formal methods for this kind of systems is greatly required. In this work, we apply a formal method that performs deductive verification on industrial smart contracts, which are self-executing digital programs. Because smart contracts manipulate cryptocurrency and transaction information, if a bug occurs in such programs, serious consequences can happen, such as a loss of money. The aim of this work is to show that a language dedicated to deductive verification, called Why3, can be a suitable language to write correct and proven contracts. We first encode existing contracts into the Why3 program; next, we formulate specifications to be proved as the absence of RunTime Error and functional properties, then we verify the behaviour of the program using the Why3 system. Finally, we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, our approach estimates the cost of gas, which is a unit that measures the amount of computational effort during a transaction.

Verification
Monday October 28, 2019, 11AM, Salle 1007
Pierre Ganty (IMDEA Software Institute) Deciding language inclusion problems using quasiorders

We study the language inclusion problem L1 ⊆ L2 where L1 is regular or context-free. Our approach checks whether an overapproximation of L1 is included in L2. Such overapproximations are obtained using quasiorder relations on words where the abstraction gives the language of all words “greater than or equal to” a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as context-free languages into regular languages and regular languages into trace sets of one-counter nets.

Verification
Monday October 21, 2019, 11AM, Salle 1007
Mohamed Faouzi Atig (Uppsala University) On Solving String Constraints

String data types are present in all conventional programming and scripting languages. In fact, it is almost impossible to reason about the correctness and security of such programs without having a decision procedure for string constraints. A typical string constraint consists of word equations over string variables denoting strings of arbitrary lengths, together with constraints on (i) the length of strings, and (ii) the regular languages to which strings belong. Decidability of this general logic is still open. In this talk, we will discuss recent results on the decidability and decision procedures for string constraints. We will focus on decision procedures that are sound and complete for a well-defined fragment of string constraints. We will also cover a technique that uses a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between these modules allows increasing the precision in an automatic manner.

Verification
Monday October 14, 2019, 11AM, Salle 1007
Laurent Doyen (LSV, ENS Paris-Saclay) Expected Finite Horizon

A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario.

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

We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.

Verification
Friday July 5, 2019, 2:30PM, Salle 1001
Mahsa Shirmohammadi (IRIF) Büchi Objectives in Countable MDPs

We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist ε-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question by constructing a non-trivial counterexample. On the other hand, we show that Markov strategies with only 1 bit of extra memory are sufficient. This work is in collaboration with Stefan Kiefer, Richard Mayr and Patrick Totzke, and is going to be presented in ICALP 2019. A full version is at https://arxiv.org/abs/1904.11573

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

Given a linear recurrence sequence (LRS), is there an algorithm that decides if the infinite sequence of numbers generated by the LRS contains 0? This is the notorious Skolem problem. The Skolem-Mahler-Lech theorem says that the set of zeros of an LRS is semi-linear; however, this doesn't translate to an algorithm, due to lack of effective bounds on the description of the zero set.

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

Processing large amounts of data used to be an affair of specialists: specialized hardware, specialized software, specialized programming model, specialized engineers. MapReduce was the first widely adopted high-level API for large-scale data processing. It helped democratize big data processing by providing a clear abstraction that was supported by several efficient systems.

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

Several recently proposed randomized testing tools for concurrent and distributed systems come with theoretical guarantees on their success. The key to these guarantees is a notion of bug depth—the minimum length of a sequence of events sufficient to expose the bug—and a characterization of d-hitting families of schedules—a set of schedules guaranteed to cover every bug of given depth d. Previous results show that in certain cases the size of a d-hitting family can be significantly smaller than the total number of possible schedules. However, these results either assume shared-memory multithreading, or that the underlying partial ordering of events is known statically and has special structure. These assumptions are not met by distributed message-passing applications.

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

Smart contract blockchains such as Ethereum and Tezos let their users program their crypto-money accounts. Bugs in these smart contracts can lead to huge losses. Yet smart contracts are necessarily small programs because checking the blockchain requires to evaluate all the smart contract calls in the history of the chain. For these reasons, smart contract languages are a good spot for formal methods.

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

Advertisement:

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.

[*] https://arxiv.org/abs/1903.09773

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

It is well-known that consensus (one-set agreement) and total order broadcast are equivalent in asynchronous systems prone to process crash failures. Considering wait-free systems, this talk addresses and answers the following question: which are the communication abstraction that “captures”, on the one hand, read/write registers, and on the other hand, k-set agreement?

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

Designing, verifying, and implementing highly reliable distributed systems is at present a hard and very labor-intensive task. Cloud-based systems have further increased this complexity due to the desired consistency, availability, scalability, and disaster tolerance. This talk addresses this challenge in the context of distributed transaction systems (DTSs) from two complementary perspectives: (i) designing DTSs in Maude with high assurance such that they satisfy desired correctness and performance requirements; and (ii) transforming verified Maude designs of DTSs into correct-by-construction distributed implementations. Regarding (i), I will talk about our Maude-based framework for automatic analysis of consistency and performance properties of DTSs. Regarding (ii), I will present a correct-by-construction automatic transformation mapping a verified formal specification of an actor-based distributed system design in Maude to a distributed implementation enjoying the same safety and liveness properties as the original formal design.

Verification
Monday April 15, 2019, 11AM, Salle 1007
John Wickerson (Imperial College London) Using Alloy to explore Weak Memory and Transactional Memory

When reasoning about concurrent programs, it is tempting to imagine that each thread executes its instructions in order, and that writes to shared memory instantly become visible to all other threads. Alas, this ideal (which is called “sequential consistency”) is rarely met. In reality, most processors and compilers allow instructions sometimes to be reordered, and loads from shared memory sometimes to retrieve stale data. This phenomenon is called “weak 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

Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are not deallocated immediately, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. We present a static type system to ensure correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.

Verification
Friday April 5, 2019, 2:30PM, Salle 3052
Cristoph Kirsch (Universität Salzburg) On the self in Selfie

Selfie is a self-contained 64-bit, 10-KLOC implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine, and (4) a prototypical symbolic execution engine that executes RISC-U symbolically. Selfie can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. Selfie has originally been developed just for educational purposes but has by now become a research platform as well. We discuss how selfie leverages the synergy of integrating compiler, target machine, and hypervisor in one self-referential package while orthogonalizing bootstrapping, virtual and heap memory management, emulated and virtualized concurrency, and even replay debugging and symbolic execution.

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:

http://selfie.cs.uni-salzburg.at

Verification
Monday March 18, 2019, 11AM, Salle 1007
Glen Mével (INRIA Paris) Time Credits and Time Receipts in Iris

I present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program’s execution time, time receipts can be used to establish a lower bound. More strikingly, time receipts can be used to prove that certain undesirable events—such as integer overflows—cannot occur until a very long time has elapsed. I will present a simple machine-checked application of time receipts, and sketch how we define our extension of Iris (and prove its soundness) in a modular way, as a layer above Iris.

Verification
Friday March 15, 2019, 11AM, Salle 3052
Sreeja Nair (LIP 6 - Sorbonne Université) Invariant safety for distributed applications

A distributed application replicates data closer to the user to ensure shorter response times and availability when the network partitions. The replicas should be able to allow updates even in case of network partitions and they send their states to converge. The application developer must also make sure that the application invariants hold true even when the replicas diverge.

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

Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in driving state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, an automated, generic, trustworthy and verification-oriented lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA.

Verification
Tuesday March 5, 2019, 11AM, 3052
Azadeh Farzan (University of Toronto) Automated Hypersafety Verification

In this talk, I will introduce an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. They can alternatively be viewed as standard safety properties of a product of the several copies of the program by itself. The key observation is that a small representative set of the product program runs, called a reduction, is sufficient to construct a formal proof. I will present an algorithm based on a counterexample-guided refinement loop that simultaneously searches for a reduction and a proof of the correctness for the reduction. The algorithm is implemented in a tool and there is evidence that itl is very effective in verifying a diverse array of hypersafety properties for a diverse class of input programs.

Verification
Monday March 4, 2019, 11AM, Salle 1007
Marie Van Den Boogard (Université Libre de Bruxelles) Beyond admissibility: Dominance between chains of strategies

In this talk, we focus on the concept of rational behaviour in multi-player games on finite graphs, taking the point of view of a player that has access to the structure of the game but cannot make assumptions on the preferences of the other players. In the qualitative setting, admissible strategies have been shown to fit the rationality requirements, as they coincide with winning strategies when these exist, and enjoy the fundamental property that every strategy is either admissible or dominated by an admissible strategy. However, as soon as there are three or more payoffs, one finds that this fundamental property does not necessarily hold anymore: one may observe chains of strategies that are ordered by dominance and such that no admissible strategy dominates any of them. Thus, to recover a satisfactory rationality notion (still based on dominance), we depart from the single strategy analysis approach and consider instead chains of strategies as families of behaviours. We establish a sufficient criterion for games to enjoy a similar fundamental property, ie, all chains are below some maximal chain, and, as an illustration, we present a class of games where admissibility fails to capture some intuitively rational behaviours, while our chain-based analysis does. Based on a joint work with N.Basset, I. Jecker, A. Pauly and J.-F. Raskin, presented at CSL'18.

Verification
Monday February 25, 2019, 11AM, Salle 1007
Pierre Courtieu (CNAM) A proof framework for mobile robots protocols

Distributed algorithms are known to be very difficult to design and certify. If these algorithms need to be fault or byzantine resilient the difficulty is even greater. Examples of flawed algorithms and proofs are numerous. It is therefore a natural domain for mechanized proofs (i.e. with the help of a proof assistant): the additional work of mechanizing the proofs should be worth the effort.

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 18, 2019, 2PM, Salle 3052
José Ignacio Requeno (Université Grenoble Alpes) Parameter Synthesis for Extended Signal Temporal Logic Specifications

Cyber-Physical Systems (CPS) are complex environments composed of embedded computers that monitor or control physical processes. Nowadays, they are ubiquitously present in most aspects of our live, ranging from power stations to communications, transport or finances. Guaranteeing a correct behaviour and a good quality of service (QoS) of such critical systems is imperative. Signal temporal logic (STL) is a specification language that is adapted for dealing with continuous time real-value properties which are characteristic in CPSs. Used in combination with formal models and model checking techniques, it allows the verification and validation of runtime executions. In this talk, I will present recent improvements in the STL language; including a new method for inferring the validity domain of parametric STL specifications.

Verification
Monday February 11, 2019, 11AM, Salle 1007
Stéphane Demri (LSV - CRNS & ENS Paris Saclay) Modal Separation Logics and Friends

Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative models is a feature shared with many modal logics such as sabotage logics, logics of public announcements or relation-changing modal logics. In the first part of the talk, we present several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. In the second part of the talk, we present the decidability status and the computational complexity of several modal separation logics, (for instance, leading to NP-complete or Tower-complete satisfiability problems). In the third part, we investigate the complexity of fragments of quantified CTL under the tree semantics (or similar modal logics with propositional quantification), some of these fragments being related to modal separation logics. Part of the presented work is done jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).

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

Concurrent languages provide weak semantics: they admit non-sequentially-consistent (SC) behaviour to accommodate weak target architectures and compiler optimisation. Subtle behaviour and intricate specifications result, but two properties help to simplify things – no thin-air values, and DRF-SC. In the first, all values must be computed from constants or inputs to the program, rather than conjured up, for example, through abuse of speculative execution. In DRF-SC, programs without data races are guaranteed SC behaviour. Unfortunately, existing languages like C/C++ admit thin-air values and DRF-SC results only apply to an unrealistic class of programs, excluding systems code and code using concurrency libraries. We provide a modular semantics that avoids thin-air values and we prove a new modular variant of DRF-SC that lifts a key barrier to its usefulness.


Year 2018

Verification
Monday December 10, 2018, 11:10AM, Salle 1007
Mahsa Shirmohammadi (LIS - CNRS & Université Aix-Marseille) On the Complexity of Value Iteration

Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal n-step payoff by iterating n times a recurrence equation which is naturally associated to the MDP. At the same time, value iteration provides a policy for the MDP that is optimal on a given finite horizon n. In this talk, we settle the computational complexity of value iteration. We show that, given a horizon n in binary and an MDP, computing an optimal policy is EXP-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. As a stepping stone, we show that it is EXP-complete to compute the n-fold iteration (with n in binary) of a function given by a straight-line program over the integers with max and + as operators.

A preliminary draft of this work is available on arXiv:

https://arxiv.org/abs/1807.04920v2

Verification
Monday December 3, 2018, 11:10AM, Salle 1007
Vincent Rahli (SnT - University of Luxembourg) Building Reliable Systems on Reliable Foundations

Current mainstream programming/verification tools are not well-suited to build safe and secure distributed programs that meet required specifications. This is a serious issue because our modern society came to heavily rely on complex and constantly evolving distributed systems that need to tolerate all kinds of threats and attacks in order to protect critical and sensitive resources. This issue is due in part to the lack of formalisms, tools, and reliable foundations. Indeed, in the past few decades, we have seen a spurt of verification tools that handle well functional sequential code, but expressive tools to reason about distributed programs are only just emerging. Moreover, a major issue with such verification tools is that they are often very complex themselves, making them error prone.

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

Agreeing on a common value in a distributed system is a problem that lies at the heart of many distributed computing problems and occurs in several flavors. Unfortunately, even modest network dynamics already prohibit solvability of exact consensus, where agents have to decide on a single output value that is within the range of the agents' initial values.

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

The BSP model (Bulk Synchronous Parallel) simplifies the construction and evaluation of parallel algorithms, with its simplified synchronization structure and cost model. Nevertheless, imperative BSP programs can suffer from synchronization errors. Programs with textually aligned barriers are free from such errors, and this structure eases program comprehension. We propose a simplified formalization of barrier inference as data flow analysis, which verifies statically whether an imperative BSP program has replicated synchronization, which is a sufficient condition for textual barrier alignment.

Verification
Monday November 5, 2018, 11:10AM, Salle 1007
Adrien Guatto (IRIF) Hierarchical Memory Management for Mutable State

It is well known that modern functional programming languages are naturally amenable to parallel programming. Achieving efficient parallelism using functional languages, however, remains difficult. Perhaps the most important reason for this is their lack of support for efficient in-place updates, i.e., mutation, which is important for the implementation of both parallel algorithms and the run-time system services (e.g., schedulers and synchronization primitives) used to execute them.

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

Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs.

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”

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.

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

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries.

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

One great issue in conceiving and specifying distributed algorithms is the sheer number of models, differing in subtle and often qualitative ways: synchrony, kind of faults, number of faults… In the context of message-passing, one solution is to restrict communication to proceed by round; A great variety of models can then be captured in the Heard-Of model, with predicates on the communication graph at each round. However, this raises another issue: how to characterize a given model by such a predicate? It depends on how to implement rounds in the model. This is straightforward in synchronous models, thanks to the upper bound on communication delay. On the other hand, asynchronous models allow unbounded message delays, which makes the implementation of rounds dependent on the specific message-passing model.

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

This paper explores the general problem of explaining the behavior of artificial neural networks (ANN). The goal is to construct a representation which enhances human understanding of an ANN as a sequence classifier, with the purpose of providing insight on the rationale behind the classification of a sequence as positive or negative, but also to enable performing further analyses, such as automata-theoretic formal verification. In particular, a probabilistic algorithm for constructing a deterministic finite automaton which is approximately correct with respect to an artificial neural network is proposed.

Verification
Friday June 29, 2018, 11AM, Salle 3052
Mahsa Shirmohammadi (LIS, CNRS - Univ. Aix-Marseille) Costs and Rewards in Priced Timed Automata

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.

Verification
Monday June 25, 2018, 11AM, Salle 3052
Nicolas Jeannerod (IRIF) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

The CoLiS project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts. The data structure that is manipulated by these scripts, namely the file system tree, is a complex one.

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

We introduce and study a new (pseudo) metric on timed words having several advantages:

- 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

Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I'll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including algebraic geometry, group theory, and quantum computing. (No previous knowledge of these fields will be assumed.)

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

In this talk, I describe the specification and proof of an (imperative, sequential) hash table implementation. The usual dictionary operations (insertion, lookup, and so on) are supported, as well as iteration via folds and iterators. The code is written in OCaml and verified using higher-order separation logic, embedded in Coq, via the CFML tool and library. This case study is part of ANR project Vocal, whose aim is to build a verified OCaml library of basic data structures.

(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

Rust is a new systems programming language, developed at Mozilla, that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features.

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

The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Verifying linearizability is a difficult, in general undecidable, problem.

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

Standard libraries of programming languages provide efficient implementations for common data containers. The details of these implementations are abstracted away by generic interfaces which are specified in terms of well understood mathematical structures such as sets, multisets, sequences, and partial functions. The intensive use of container libraries makes important their formal verification.

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

We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called \emph{Synchronized Dynamic Pushdown Networks} (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to a Counter-Example Guided Abstraction Refinement (CEGAR) scheme, using multiple abstractions of increasing complexity and precision.

Verification
Monday April 9, 2018, 11AM, Salle 1007
Ilya Sergey (University College London, UK) Programming and Proving with Distributed Protocols

Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on top of a two-phase commit instance). Recent work has developed several approaches for addressing (a) by means of mechanically verifying implementations of core distributed components, but no methodology exists to address (b) by composing such verified components into larger verified applications.

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

The applied pi-calculus is a powerful framework to model protocols and to define security properties. In this symbolic model, it is possible to verify automatically complex security properties such as strong secrecy, anonymity and unlinkability properties which are based on equivalence of processes. In this talk, we will see an overview of a verification method used by a tool, Akiss. The tool is able to handle

- 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

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into omega-automata by elementary means. In particular, the breakpoint, Safra, and ranking constructions used in other translations are not needed.

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

Random testing has proven to be an effective way to catch bugs in distributed systems. This is surprising, as the space of executions is enormous. We provide a theoretical justification of the effectiveness of random testing under various “small depth” hypotheses. First, we show a general construction, using the probabilistic method from combinatorics, that shows that whenever a random test covers a fixed coverage goal with sufficiently high probability, a small randomly-chosen set of tests achieves full coverage with high probability. In particular, we show that our construction can give test sets exponentially smaller than systematic enumeration. Second, based on an empirical study of many bugs found by random testing in production distributed systems, we introduce notions of test coverage which capture the “small depth” hypothesis and are empirically effective in finding bugs. Finally, we show using combinatorial arguments that for these notions of test coverage we introduce, we can find a lower bound on the probability that a random test covers a given goal. Our general construction then explains why random testing tools achieve good coverage—and hence, find bugs—quickly.

Verification
Monday March 12, 2018, 11AM, Salle 1007
Thomas Colcombet (IRIF & CNRS) Automata and Program Analysis

This will be a presentation of a collaboration with Laure Daviaud and Florian Zuleger. We show how recent results concerning quantitative forms of automata help providing refined understanding of the properties of a system (for instance, a program). In particular, combining the size-change abstraction together with results concerning the asymptotic behavior of tropical automata yields extremely fine complexity analysis of some pieces of code.

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

We propose a new formal criterion for secure compilation, giving strong end-to-end security guarantees for software components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model _dynamic_ compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others—in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees up to the point when it becomes compromised, after which an attacker can take complete control over the component and use any of its privileges to attack the remaining uncompromised components. More precisely, we ensure that dynamically compromised components cannot break the safety properties of the system at the target level any more than equally privileged components without undefined behavior already could in the source language.

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.

Classical results from algebra, such as Hilbert's Basis Theorem and Hilbert’s Nullstellensatz, have been used to decide equivalence for some classes of transducers, such as HDT0L (Honkala 2000) or more recently deterministic tree-to-string transducers (Seidl, Maneth, Kemper 2015). In this talk, we propose an abstraction of these methods. The goal is to investigate the scope of the “Hilbert method” for transducer equivalence that was described above.

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”

Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However, in absence of further justification, the guarantees only hold for the language (source, target, or intermediate representation) on which the analysis is performed.

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

We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret. In a probabilistic and nondeterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.

Verification
Monday January 22, 2018, 11AM, Salle 1007
Josef Widder (TU Wien) Synthesis of Distributed Algorithms with Parameterized Thresholds Guards

Fault-tolerant distributed algorithms are notoriously hard to get right. I present an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts. In particular, I will consider threshold-based distributed algorithms, where a process has to wait until the number of messages it receives reaches a certain threshold, in order to perform an action. Such algorithms are typically used for achieving fault tolerance in distributed algorithms for broadcast, atomic commitment, or consensus. Using this method, one can synthesize distributed algorithms that are correct for every number n of processes and every number t of faults, provided some resilience condition holds, e.g., n > 3t. This approach combines recent progress in parameterized model checking of distributed algorithms—which I also address—with counterexample-guided synthesis.

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

Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications like task scheduling or discrete event simulation, and show that verifying linearizability of such implementations is reducible to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues with an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.

Verification
Monday January 8, 2018, 11AM, Salle 1007
Jean-Jacques Lévy (IRIF & INRIA) Proofs of graph algorithms with automation and their readability

In this talk, we present a proof of correctness for an algorithm computing strongly connected components in a directed graph by Tarjan [1972]. It will be the starting point of a discussion about the readability of formal proofs. This proof was achieved with the Why3 system and the Coq/ssreflect proof assistant. The same proof was redone fully in Coq/ssreflect and Isabelle/HOL.

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

Looking at some monoids and (semi)rings (natural numbers, integers and p-adic integers), and more generally, residually finite algebras (in a strong sense), we prove the equivalence of two ways for a function on such an algebra to behave like the operations of the algebra. The first way is to preserve congruences or stable preorders. The second way is to demand that preimages of recognizable sets belong to the lattice or the Boolean algebra generated by the preimages of recognizable sets by “derived unary operations” of the algebra (such as translations, quotients,…).

Verification
Thursday December 7, 2017, 4PM, Salle 1007
Luke Ong (University of Oxford) Constrained Horn clauses for automatic program verification: the higher-order case

Following Björner, McMillan and Rybalchenko, we develop an approach to the automatic verification of higher-order functional programs based on constrained Horn clauses. We introduce constrained Horn clauses in higher-order logic, and decision problems concerning their satisfiability and the safety verification of higher-order programs. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained via a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that an extension of the decision problem in which refinement types are used directly as guards on existential quantifiers can be reduced to the original problem. This result can be used to show that properties of higher-order functions that are definable using refinement types are also expressible using higher-order constrained Horn clauses. (Joint work with Toby Cathcart Burn and Steven Ramsay.)

Verification
Tuesday November 28, 2017, 1:30PM, Salle 3052
Léon Gondelman (Radboud University, The Netherlands) The Spirit of Ghost Code

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge.

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

Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthezing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler’s method is the most basic technique for approximating such solutions. We present here an estimation of the Euler’s method local error, using the notion of “one-sided Lispchitz constant’’ for modes. This yields a general synthesis approach which can encompass uncertain parameters, local information and stochastic noise.

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

I will present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C/C++11 memory model without dependency cycles. Unlike previous approaches, which enumerate thread interleavings up to some partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and applied it to a number of challenging concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools, and is also more resilient to small changes in the benchmarks.

(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

Linearizability is the standard correctness criterion for concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.

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

Numerous contributions have been made for some years to allow users to exchange formal proofs between different provers. The main propositions consist in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a common formalism in which proofs can be translated and combined. To relate the independently developed mathematical libraries used in proof assistants, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems called MathTransfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.

Verification
Monday October 16, 2017, 11AM, Salle 1007
Noam Rineztky (Tel-Aviv University) Verifying Equivalence of Spark Programs

Apache Spark is a popular framework for writing large scale data processing applications. Our long term goal is to develop automatic tools for reasoning about Spark programs. This is challenging because Spark programs combine database-like relational algebraic operations and aggregate operations, corresponding to (nested) loops, with User Defined Functions (UDFs).

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

Paper: http://www.cs.tau.ac.il/~maon/pubs/2017-cav.pdf

Verification
Monday October 9, 2017, 11AM, Salle 1007
Javier Esparza (Technische Universität München) Polynomial Analysis Algorithms for Free-Choice Workflow Nets

Workflow Petri nets are a successful formalism for modelling, simulating, and analyzing business processes. In this area, free-choice workflow nets play an important role: Core formalisms for business processes can be translated into free-choice nets, and many industrial models are free-choice.

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

We define a correctness criterion, called robustness against concurrency, for a class of event-driven asynchronous programs that are at the basis of modern UI frameworks in Android, iOS, and Javascript. A program is robust when all possible behaviors admitted by the program under arbitrary procedure and event interleavings are admitted even if asynchronous procedures (respectively, events) are assumed to execute serially, one after the other, accessing shared memory in isolation. We characterize robustness as a conjunction of two correctness criteria: event-serializability (i.e., events can be seen as atomic) and event-determinism (executions within each event are insensitive to the interleavings between concurrent tasks dynamically spawned by the event). Then, we provide efficient algorithms for checking these two criteria based on polynomial reductions to reachability problems in sequential programs. This result is surprising because it allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity. We demonstrate via case studies on Android apps that the typical mistakes programmers make are captured as robustness violations, and that violations can be detected efficiently using our approach.

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

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve higher-order concepts such as set cardinalities, arithmetic, and complex quantification.

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

In this talk we present a new approach for verification for configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools. We describe a framework which analyzes data sets of correct configuration files and synthesizes rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.

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

We present an abstract framework for verifying concurrent algorithms on search data structures that support dictionaries. The framework can be specialized to every search data structure we know, from linked lists to complex B-trees. We obtain this framework by instantiating RGSep, which is a program logic that combines rely-guarantee reasoning and separation logic. RGSep is parameterized by a so-called resource algebra, which is typically the standard heap model of separation logic. Instead of using the standard heap model, we develop a new resource algebra that enables compositional reasoning about search graphs. Using this search graph model, we obtain simple correctness proofs of complex concurrent dictionary algorithms. The algorithms and proofs abstract from the specific search data structure that the algorithm operates on and can then be refined to a concrete data structure implementation.

Verification
Tuesday June 6, 2017, 11AM, Salle 3052
Sergio Rajsbaum (UNAM Mexico) Tasks, objects, and the notion of a distributed problem

The universal computing model of Turing, which was central to the birth of modern computer science, identified also the essential notion of a problem, as an input output function to be computed by a Turing machine. In distributed computing, \emph{tasks} are the equivalent of a function: each process gets only part of the input, and computes part of the output after communicating with other processes.

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

This work presents a novel approach for automatically repairing an erroneous program with respect to a given set of assertions. Programs are repaired using a predefined set of mutations. We refer to a bounded notion of correctness, even though, for a large enough bound all returned programs are fully correct. To ensure no changes are made to the original program unless necessary, if a program can be repaired by applying a set of mutations $Mut$, then no superset of $Mut$ is later considered. Programs are checked in increasing number of mutations, and every minimal repaired program is returned as soon as found.

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

The last decade has seen renewed interest in automated techniques for proving the termination of programs. A popular termination criterion is based on the covering of the transitive hull of the transition relation of a program by a finite number of well-founded relations. In an automated analysis, this termination criterion is usually established by an inductive proof using transition predicate abstraction. Such termination proofs have the structure of a finite automaton. These automata, which we call transition automata, are the central object of study in this talk. Our main results are as follows: (1) A previous criterion for termination analysis with transition automata is not complete; we provide a complete criterion. (2) We show how to bound the height of the transition relation of the program using the termination proof by transition predicate abstraction. This result has applications in the automated complexity analysis of programs. (3) We show that every termination proof by transition predicate abstraction gives rise to a termination proof by the size-change abstraction; this connection is crucial to obtain results (1) and (2) from previous results on the size-change abstraction. Further, our result establishes that transition predicate abstraction and size-change abstraction have the same expressivity for automated termination proofs.

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.

We present the ideal framework which was recently used to obtain new deep results on Petri nets and extensions. We will present the proof of the famous but unknown Erdös-Tarski theorem. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm.

Verification
Monday March 27, 2017, 11AM, Salle 1007
Mohamed Faouzi Atig (Uppsala University) Lossy Channel Systems with Data.

Lossy channel systems are a classical model with applications ranging from the modelling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this talk, we present two extensions of lossy channel systems. In the first part of the talk, we extend lossy channel systems by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of Timed Lossy Channel Systems (TLCS). We show that the state reachability problem is decidable for TLCS.

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

Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards “the good thing” rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program. This is joint work with Azadeh Farzan and Zachary Kincaid and published at LICS 2016 (http://www.cs.princeton.edu/~zkincaid/pub/lics16.pdf)

Verification
Monday March 13, 2017, 11AM, Salle 1007
Ori Lahav (MPI Kaiserslautern) A Promising Semantics for Relaxed-Memory Concurrency

Despite many years of research, it has proven very difficult to develop a memory model for concurrent programming languages that adequately balances the conflicting desiderata of programmers, compilers, and hardware. In this paper, we propose the first relaxed memory model that (1) accounts for nearly all the features of the C++11 concurrency model, (2) provably validates a number of standard compiler optimizations, as well as a wide range of memory access reorderings that commodity hardware may perform, (3) avoids bad “out-of-thin-air” behaviors that break invariant-based reasoning, (4) supports “DRF” guarantees, ensuring that programmers who use sufficient synchronization need not understand the full complexities of relaxed-memory semantics, and (5) defines the semantics of racy programs without relying on undefined behaviors, which is a prerequisite for applicability to type-safe languages like Java. The key novel idea behind our model is the notion of promises: a thread may promise to execute a write in the future, thus enabling other threads to read from that write out of order. Crucially, to prevent out-of-thin-air behaviors, a promise step requires a thread-local certification that it will be possible to execute the promised write even in the absence of the promise. To establish confidence in our model, we have formalized most of our key results in Coq.

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

Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated.

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

In this talk I will present some of the research I have been involved in concerning the specification and monitoring of timed, continuous and hybrid behaviors using formalism such as Signal Temporal Logic and Timed Regular Expressions. I will discuss the similarities and differences between properties/assertions and other “measures” which are used in many application domains to evaluate behaviors, as well as the difference between monitoring real systems during their execution and monitoring simulated models during the system design phase.

Verification
Monday February 20, 2017, 11AM, Salle 1007
Loig Jezequel (L2SN - Nantes) Lazy Reachability Analysis in Distributed Systems

We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in a first prototype and provide some very encouraging experimental results.

Verification
Monday January 23, 2017, 11AM, Salle 1007
Andrea Cerone (Imperial College London) Analysing Snapshot Isolation

Snapshot isolation (SI) is a widely used consistency model for transaction processing, implemented by most major databases and some of transactional memory systems. Unfortunately, its classical definition is given in a low-level operational way, by an idealised concurrency-control algorithm, and this complicates reasoning about the behaviour of applications running under SI. We give an alternative specification to SI that characterises it in terms of transactional dependency graphs of Adya et al., generalising serialization graphs. Unlike previous work, our characterisation does not require adding additional information to dependency graphs about start and commit points of transactions. We then exploit our specification to obtain two kinds of static analyses. The first one checks when a set of transactions running under SI can be chopped into smaller pieces without introducing new behaviours, to improve performance. The other analysis checks whether a set of transactions running under a weakening of SI behaves the same as when it running under SI.


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)

We propose a hierarchical abstract domain for the analysis of free list memory allocators that tracks shape and numerical properties about both the heap and the free lists. Our domain is based on Separation Logic extended with predicates that capture the pointer arithmetics constraints for the heap list and the shape of the free list. These predicates are combined using a hierarchical composition operator to specify the overlapping of the heap list by the free list. In addition to expressiveness, this operator leads to a compositional and compact representation of abstract values and simplifies the implementation of the abstract domain. The shape constraints are combined with numerical constraints over integer arrays to track properties about the allocation policies (best-fit, first-fit, etc). Such properties are out of the scope of the existing analyzers. We implemented this domain and we show its effectiveness on several implementations of free list allocators.

Verification
Friday December 9, 2016, 11AM, Salle 3052
Alastair Donaldson (Imperial College London) Exposing Errors Related to Weak Memory in GPU Applications

In this presentation, I will describe a project led by my PhD student Tyler Sorensen, on the systematic design of a testing environment that uses stressing and fuzzing to reveal errors in GPU applications that arise due to weak memory effects. This approach is evaluated across several CUDA applications that use fine-grained concurrency, on seven GPUs spanning three Nvidia architectures. The results show that applications that rarely, or never, exhibit errors related to weak memory when executed natively can readily exhibit these errors when executed in the testing environment. The testing environment also provides a means to identify the root causes of erroneous weak effects, and automatically suggests how to insert fences that experimentally eliminate these errors. This empirical fence insertion method carries significantly lower overhead, in terms of execution time and energy consumption, than a more conservative, guaranteed-sound approach.

Verification
Monday December 5, 2016, 11AM, Salle 1007
Guilhem Jaber (IRIF) SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence

Operational Techniques (Kripke Logical Relations and Environmental/Open/Parametric Bisimulations) have matured enough to become now formidable tools to prove contextual equivalence of effectful higher-order programs. However, it is not yet possible to automate such proofs – the problem being of course in general undecidable. In this talk, we will see how to take the best of these techniques to design an automatic procedure which is able many non-trivial examples of equivalence, including most of the examples from the literature. The talk will describe the main ingredients of this method: - Symbolic reduction to evaluate of programs, - Transition systems of heap invariants, as used with Kripke Logical Relations, - Temporal logic to abstract over the control flow between the program and its environment, - Circular proofs to automate the reasoning over recursive functions. Using them, we will see how we can reduce contextual equivalence to the problem of non-reachability in some automatically generated transition systems of invariants.

Verification
Monday November 28, 2016, 11AM, Salle 1007
Georg Zetzsche (LSV, ENS Cachan) First-order logic with reachability for infinite-state systems

First-order logic with the reachability predicate (FOR) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).

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

Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We propose a parameterizable code-to-code translation to generate a set of simpler program variants such that each interleaving of the program is captured by at least one of them. These variants can then be checked autonomously in parallel. Our approach is independent of the tool that is chosen for the final analysis, it is compatible with weak memory models, and it amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We do our experiments using Lazy-CSeq as off-the-shelf final verifier and demonstrate that our approach is able to find bugs in the hardest known concurrency benchmarks in a matter of minutes where other dynamic and static tools fail to conclude.

Verification
Monday November 14, 2016, 11AM, Salle 1007
Philipp Rümmer (University of Uppsala) Liveness of Randomised Parameterised Systems under Arbitrary Schedulers

e consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including unfair) schedulers, which is often considered a desirable property in the literature of self-stabilising systems. In this paper we introduce an automatic method of proving liveness for randomised parameterised systems under arbitrary schedulers. Viewing liveness as a two-player reachability game (between Scheduler and Process), our method is a CEGAR approach that synthesises a progress relation for Process that can be symbolically represented as a finite-state automaton. The method incrementally constructs a progress relation, exploiting both Angluin's $L*$ algorithm and SAT-solvers. Our experiments show that our algorithm is able to prove liveness automatically for well-known randomised distributed protocols, including Lehmann-Rabin Randomised Dining Philosopher Protocol and randomised self-stabilising protocols (such as the Israeli-Jalfon Protocol). To the best of our knowledge, this is the first fully-automatic method that can prove liveness for randomised protocols.

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

Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable. However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.

Joint work with Jérôme Leroux.

Verification
Monday October 10, 2016, 11AM, Salle 1007
Steven de Oliveira (CEA) Polynomial invariants by linear algebra

One of the main issue in formal verification is the analysis of loops, considered as a major research problem since the 70s. Program verification based on Floyd-Hoare's inductive assertion and CEGAR-like techniques for model-checking uses loop invariants in order to reduce the problem to an acyclic graph analysis instead of unrolling or accelerating loops.

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

To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. In this talk I will present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability, and I will focus on a consistency model called Parallel Snapshot Isolation. The results I will outline handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.

Verification
Monday September 26, 2016, 11AM, Salle 1007
Arnaud Sangnier (IRIF) Fixpoints in VASS: Results and Applications

VASS (Vector Addition Systems with States), which are equivalent to Petri nets, are automata equipped with natural variables that can be decremented or incremented. VASS are a powerful model which has been intensively studied in the last decades. Many verification techniques have been developed to analyse them and the frontier between the decidable and undecidable problems related to VASS begins to be well known. One interesting point is that the model-checking of linear temporal logics (like LTL or linear mu-calculus) is decidable for this model but this is not anymore the case when considering branching time temporal logics. However some restrictions can be imposed on the logics and on the studied system in order to regain decidability. In this talk, we will present these results concerning the model-checking of VASS and the techniques leading to the decidability results. We will then show how these techniques and results can be used to analyse some extensions of VASS with probabilities, namely probabilistic VASS and VASS Markov Decision Processes.

Verification
Monday September 19, 2016, 11AM, Salle 1007
Francesco Belardinelli (Université d'Evry) Abstraction-based Verification of Infinite-state Data-aware Systems

Data-aware Systems (DaS) are a novel paradigm to model business processes in Service-oriented Computing.

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?

ubstantial research efforts have been devoted to tools for reasoning about -and proving properties of- programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.

Verification
Monday March 14, 2016, 11AM, Salle 1007
Paul Gastin (LSV) Formal methods for the verification of distributed algorithms

We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete. Based on a joint work with C. Aiswarya and Benedikt Bollig, extended abstract at CONCUR’15: http://www.lsv.ens-cachan.fr/~gastin/mes-publis.php?onlykey=ABG-concur15.

Verification
Monday March 7, 2016, 11AM, Salle 1007
Julien Signoles (CEA-LIST) Frama-C, a collaborative and extensible framework for C code analysis

Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, testing and monitoring, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This talk presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. It focuses on its specification language ACSL, and on different ways to verify ACSL specifications through static and dynamic analyses.

Verification
Monday February 29, 2016, 11AM, Salle 1007
Pierre Fraigniaud (IRIF) Fault-Tolerant Decentralized Runtime Monitoring

Runtime verification is aiming at extracting information from a running system, and using it to detect and possibly react to behaviors violating a given correctness property. Decentralized runtime verification involves a set of monitors observing the behavior of the underlying system. In this talk, the investigation of decentralized runtime verification in which not only the elements of the observed system, but also the monitors themselves are subject to failures will be presented. In this context, it is unavoidable that the unreliable monitors may have different views of the underlying system, and therefore may have different valuations of the correctness property. We characterize the number of valuations required for monitoring a given correctness property in a decentralized manner. Our lower bound is independent of the logic used for specifying the correctness property, as well as of the way the set of valuations returned by the monitors is globally interpreted. Moreover, our lower bound is tight in the sense that we design a distributed protocol enabling any given set of monitors to verify any given correctness property using as many different valuations as the one given by this lower bound. Joint work with: Sergio Rajsbaum (UNAM, Mexico) and Corentin Travers (LaBRI, Bordeaux).