### Vérification

** Date et lieu :** le lundi à 11h, salle 1007, Sophie Germain

** Responsables :** Ahmed Bouajjani, Constantin Enea et Arnaud Sangnier

Mercredi 28 juin 2017 · 14h00 · Salle 3052

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

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

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

Jeudi 22 juin 2017 · 11h00 · Salle 3052

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

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

Lundi 12 juin 2017 · 14h00 · Salle 3052

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

Mardi 06 juin 2017 · 11h00 · Salle 3052

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

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

Jeudi 01 juin 2017 · 11h00 · Salle 3052

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

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

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

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

Mardi 23 mai 2017 · 15h30 · Salle 3052

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

Lundi 22 mai 2017 · 11h00 · Salle 1007

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

Lundi 27 mars 2017 · 11h00 · Salle 1007

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

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

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

Lundi 20 mars 2017 · 11h00 · Salle 1007

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

Lundi 13 mars 2017 · 11h00 · Salle 1007

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

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

Lundi 06 mars 2017 · 11h00 · Salle 1007

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

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

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

Lundi 27 février 2017 · 11h00 · Salle 1007

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

Lundi 20 février 2017 · 11h00 · Salle 1007

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

Lundi 23 janvier 2017 · 11h00 · Salle 1007

Andrea Cerone (Imperial College London) · Analysing Snapshot Isolation

Lundi 12 décembre 2016 · 11h00 · Salle 1007

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

Vendredi 09 décembre 2016 · 11h00 · Salle 3052

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

Lundi 05 décembre 2016 · 11h00 · Salle 1007

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

Lundi 28 novembre 2016 · 11h00 · Salle 1007

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

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

Jeudi 24 novembre 2016 · 15h00 · Salle 3052

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

Lundi 14 novembre 2016 · 11h00 · Salle 1007

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

Joint work with Anthony W. Lin.

Lundi 24 octobre 2016 · 11h00 · Salle 1007

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

Joint work with Jérôme Leroux.

Lundi 10 octobre 2016 · 11h00 · Salle 1007

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

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

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

Lundi 03 octobre 2016 · 11h00 · Salle 1007

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

Lundi 26 septembre 2016 · 11h00 · Salle 1007

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

Lundi 19 septembre 2016 · 11h00 · Salle 1007

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

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

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

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

Lundi 30 mai 2016 · 11h00 · Salle 1007

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

**29-02-2016** : Pierre Fraignaud (IRIF), **Fault-Tolerant Decentralized Runtime Monitoring**

- **Abstract :**
*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)*

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

- **Abstract :***
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. *

**14-03-2016** : Paul Gastin (LSV), ** Formal methods for the verification of distributed algorithms **

- **Abstract :***
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
*