FRIDA 2017
The 4^{th} Workshop on
Formal Reasoning in Distributed Algorithms (FRIDA 2017)
October 16, 2017 (room Edison I)
Satellite workshop of DISC 2017 (Vienna, Austria)
Last minute updates:
 The lunch schedule of FRIDA aligns with the other workshops: the lunch time is 12:3014:00.
 The talk by Maria PotopButucaru starts at 14:00.
 The talk by Tali Sznajder starts at 14:30.
 The talk by Sylvain Conchon starts at 15:00.
 The talk on “Verifying Faulttolerance in Parameterised MultiAgent Systems” will be given by Edoardo Pirovano at 17:30.
Please do not forget to register for FRIDA’17 at the DISC’17 registration page.
Preliminary program
See the abstracts below
08:30  Alexey Gotsman 
Modular verification of consensus protocols

09:00  Ahmed Bouajjani  Verifying EventDriven Asynchronous Programs against Concurrency 
09:30  Christoph Sprenger  The verification of a secure internet architecture 
10:00  Ezio Bartocci  Monitoring Mobile and Spatially Distributed CyberPhysical Systems 
10:30 – 11:00 coffee break 

11:00  Sergio Rajsbaum  Tasks, objects, and the notion of a distributed problem 
11:30  Pierre Fraigniaud  On the various aspects of distributed decision 
12:00  Gustavo Petri (U Paris 7)  Strong Invariants for Weak Consistency 
12:30 – 14:00 lunch break 

14:00  Maria PotopButucaru  Models for mobile robots from continus to discrete spaces 
14:30  Tali Sznajder  Parameterized Verification of Algorithms for Oblivious Robots on a Ring 
15:00  Sylvain Conchon  Cubicle : a model checker for parameterized arraybased transition systems 
15:30 – 16:00 coffee break 

16:00  Cezara Dragoi  Partially synchronous programming abstractions for replicated state machine 
16:30  Thibaut Balabonski  Certified Gathering of Oblivious Mobile Robots 
17:00  Philippe Queinnec  Describing asynchronous communications in distributed algorithms 
17:30  Edoardo Pirovano  Verifying Faulttolerance in Parameterised MultiAgent Systems 
Summary of the workshop
Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safetycritical control systems. Whereas many applications are of critical importance, the correctness of distributed algorithms is usually based on very subtle mathematical arguments. Consequently, one easily can make mistakes with handwritten proofs, which reduces the trust in the correctness of these systems.
In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computeraided veriﬁcation of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required.
The topics of interest for the third FRIDA workshop are:
 models for distributed algorithms
 model checking
 proof assistants & theorem proving
 parameterized model checking
 integration of different verification techniques
 concurrency
 distributed algorithm theory
 benchmark distributed algorithms
 fault tolerance
 synthesis
 automated code generation for distributed systems
 runtime verification of distributed systems
Confirmed Speakers
 Sergio Rajsbaum. Tasks, objects, and the notion of a distributed problem.
 Christoph Sprenger. The verification of a secure internet architecture.
 Pierre Fraigniaud. On the various aspects of distributed decision.
 Maria PotopButucaru. Models for mobile robots from continus to discrete spaces.
 Ahmed Bouajjani. Verifying EventDriven Asynchronous Programs against Concurrency.
 Edoardo Pirovano & Alessio Lomuscio. Verifying Faulttolerance in Parameterised MultiAgent Systems.
 Ezio Bartocci. Monitoring Mobile and Spatially Distributed CyberPhysical Systems.
 Alexey Gotsman. Modular verification of consensus protocols.
 Gustavo Petri. Strong Invariants for Weak Consistency
 Philippe Quéinnec. Describing asynchronous communications in distributed algorithms.
 Tali Sznajder. Parameterized Verification of Algorithms for Oblivious Robots on a Ring.
 Cezara Drăgoi. Partially synchronous programming abstractions for replicated state machine
 Thibaut Balabonski. Certified Gathering of Oblivious Mobile Robots.
 Sylvain Conchon. Cubicle : a model checker for parameterized arraybased transition systems
Abstracts
Ezio Bartocci (TU Wien, Austria). Monitoring Mobile and Spatially Distributed CyberPhysical Systems.
CyberPhysical Systems (CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, spatial along with the temporal requirements play an essential role for their correct and safe execution. However, the local interactions among the system components result in global spatiotemporal emergent behaviors often impossible to predict at the design time. In this work we pursue a complementary approach by introducing STREL a novel spatiotemporal logic that enable the specification of spatiotemporal requirements and to monitor them over executions of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic with two novel spatial operators reach and escape from which is possible to derive other spatial modalities such as everywhere, somewhereand surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbours, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimisation. We prove that for certain models, all the spatial properties expressed with reach and escape using euclidean distance satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for STREL and to demonstrate the feasibility of our approach, we show its application using the monitoring of a simulated mobile adhoc sensor network as our running example.
Thibaut Balabonski (Université Paris Sud & LRI, France). Certified Gathering of Oblivious Mobile Robots.
Swarms of mobile robots have recently attracted the focus of the Distributed Computing community. One of the fundamental problems in this context is that of gathering the robots: the robots must meet at a common location, not known beforehand. Despite its apparent simplicity, this problem proved quite hard to characterise fully, due to many model variants, leading to informal errorprone reasoning.
Over the past few years, a significant effort has resulted in the set up of a formal framework, relying on the Coq proof assistant, that was used to provide certified results related to the gathering problem. We will see the main abstractions that permit to reason about oblivious mobile robots that evolve in a bidimensional Euclidean space, the distributed executions they can perform, and the variants of the gathering problem they can solve or they cannot solve.
This talk will present several models for mobile robots networks starting with mobile robots in 2D and 3D continuos spaces and finishing with robots in discrete spaces. The talk would like to brig to the attention of formal methods community these models for two main reasons. First, many distributed algorithms in these models are difficult to prove especially when the system is asynchronous. Second, many problems are open and solutions are difficult to find manually. We advocate that these models can heavily benefit from the expertise of formal methods community.
Ahmed Bouajjani (Univ. Paris Diderot (Paris 7), France). Verifying EventDriven Asynchronous Programs against Concurrency.
We define a correctness criterion, called robustness against concurrency, for a class of eventdriven 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
This is a joint work with Michael Emmi, Constantin Enea, Burcu KulahciogluOzkan, and Serdar Tasiran.
Sylvain Conchon (Université ParisSud 11, France). Cubicle : a model checker for parameterized arraybased transition systems.
In this talk, I will present Cubicle, a model checker for verifying safety properties of arraybased systems, a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. After a short presentation of the semantics of its input language, I will present some details about its implementation, mainly its symbolic backward reachability analysis which makes use of Satisfiabilty Modulo Theories. I will conclude with a presentation of current and future works.
Cezara Drăgoi (INRIA & ENS Paris, France). Partially synchronous programming abstractions for replicated state machine.
Replication is the standard way to make distributed applications faulttolerant. Implementing state machine replication is notoriously difficult due to asynchronous communication and the occurrence of faults, such as the network dropping messages or processes crashing.
One fundamental obstacle in having correct faulttolerant implementations is the lack of abstractions when reasoning about their behaviors. In this talk we focus on partially synchronous programming abstractions that view asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. This view simplifies the proof arguments making systems amendable to automated verification.
Technically, we take a programming language perspective and define a domain specific language which has a partially synchronous semantics and separates the implementation of network constraints from the algorithmic computation done by processes. We validate our technique by defining partially synchronous abstractions for several state machine replication algorithms, enabling automation of the verification procedure.
Pierre Fraigniaud (CNRS, France). On the various aspects of distributed decision.
This talk will survey various aspects of distributed decision, and their impacts on the theory of distributed computing, as well as their applications to distributed verification and robust computing. Distributed decision is characterized by a distributed system formed by collection of computing entities connected via some medium of communication, and a system predicate potentially expressed using specific logics. The computing entities must collectively determine whether the system is in a correct state with respect to the predicate. Distributed decision has been the subject of an abundant literature during the last decade. This talk will survey this literature, in classifying the different approaches of distributed decision, and their potential applications to related fields such as distributed system verification and faulttolerant distributed computing.
Alexey Gotsman (IMDEA Software Institute, Spain). Modular verification of consensus protocols.
TBA
Edoardo Pirovano and Alessio Lomuscio (Imperial College London, UK). Verifying Faulttolerance in Parameterised MultiAgent Systems.
The talk will be given by Edoardo Pirovano.
I will present a method to evaluate the faulttolerance of a multiagent system whose number of agents is unknown at design time. Specifically, I will present a technique for injecting a variety of nonideal behaviours, or faults, studied in the safetyanalysis literature into the abstract agent templates that are used to generate an unbounded family of multiagent systems with different sizes. We will define the parameterised faulttolerance problem as the decision problem of establishing whether any concrete system, in which the ratio of faulty versus nonfaulty agents is under a given threshold, satisfies a given temporalepistemic specification. I will describe a sound and complete technique for solving the problem for the semantical setup considered. I will also present an implementation and a case study identifying the threshold under which the alpha swarm aggregation algorithm is robust to faults against its temporalepistemic specifications.
Joint work with Panagiotis Kouvaros
Gustavo Petri (Université Paris Diderot — Paris 7, France). Strong Invariants for Weak Consistency.
In this talk I will explore different weak consistency criteria from the standpoint of the invariants that they can guarantee without additional programmer instrumentation. I will show how some invariants are related to the guarantees provided by the different criteria, and how they help to compare and classify these criteria.
This is joint work with Marc Shapiro and Masoud SaeidaArdekani.
Philippe Quéinnec (INPT/ENSEEIHT & IRIT, France). Describing asynchronous communications in distributed algorithms.
To formally study a distributed algorithm, a obvious requirement is to have a formal specification of this algorithm. This specification can come from an informal description of the algorithm, from an algorithmic description, from the derivation of an abstract specification (e.g. by refinement)… Anyway, at one point, the distributed nature of the algorithm appears, with nodes or sites interacting with each other. At the lowest level, when deployed on a set of computers, this communication is implemented with messages on a network. However, to reason about the algorithm, the intricate and gloomy details of the interface and behavior of this network is uninteresting. Thus researchers have invented lots of different ways to describe communication. For instance, one can use shared variables with an adequate data structure to hold the messages, e.g. a set or a queue. This yields the question of choosing the right data structure, both for the correct specification of the algorithm and for an easier reasoning. This in turn gives rise to several questions on unexpected or undesired properties of the chosen representation. Order of delivery, fairness of delivery, atomicity of communication actions, nondeterminism, size boundness or failures are often embedded in this representation, and it is not always clear if they are wanted or needed.
In this talk, I will present some classic ways of representing asynchronous communication and I will discuss their pitfalls. I will also present an approach we have developed to allow for a simple parameterization of the communication properties.
Sergio Rajsbaum (Universidad Nacional Autonoma de Mexico, 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, 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 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 give a short overview of our work on intervallinearizability, 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.
Joint work with Armando Castañeda and Michel Raynal
Christoph Sprenger (ETH Zürich, Switzerland). The verification of a secure internet architecture.
Routing is at the heart of the Internet and has been a continual source of security problems since its expansion in the 1980s. SCION is a new approach to the Internet, which offers dramatically better security properties than we currently have. We describe a collaborative effort, the Verified SCION Project, at ETH Zurich that aims to verify SCION, going the full distance from highlevel networkwide properties down to the code running on SCION routers. We will explain the issues involved, the approach we take, the progress we have made, and perspectives for the future.
The work reported on is joint work between three groups at ETH Zurich: our Information Security Group lead by David Basin, the Network Security Group of Adrian Perrig, and the Programming Methodology Group of Peter Mueller.
Tali Sznajder (LIP6, France). Parameterized Verification of Algorithms for Oblivious Robots on a Ring.
We study verification problems for autonomous swarms of mobile robots that selforganize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be errorprone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameterized case. We show that safety and reachability problems are undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the synchronous case for a particular class of algorithms. Several properties on the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMTsolver. Feasibility of our approach is demonstrated by the encoding of several case studies. Results published in FMCAD’17.
Organization
 Swen Jacobs (Saarland University)
 Igor Konnov (TU Wien)
 Stephan Merz (INRIA Nancy & LORIA)
 Josef Widder (TU Wien)
Previous editions
Starting a productive dialogue between distributed algorithms and verification communities was the goal of a successful Dagstuhl Seminar “Formal Verification of Distributed Algorithms” which was held in April 2013. During this seminar, the participants agreed that a series of workshops should be held in order to strengthen the community that does research on these issues. The 1^{st} workshop on Formal Reasoning in Distributed Algorithms took place in Vienna as part of the Vienna Summer of Logic’14 and Federated Logic Conference’14. The 2^{nd} FRIDA workshop took place in Grenoble as part of FORTE’15. The 3^{rd} FRIDA workshop was organized in Marrakech as part of NETYS’16.