### Vérification

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

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

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
*