FRIDA 2017


The 4th Workshop on

Formal Reasoning in Distributed Algorithms (FRIDA 2017)

October 16, 2017

Satellite workshop of DISC 2017 (Vienna, Austria)


Important Dates

Workshop date October 16, 2017

Summary of the workshop

Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safety-critical 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 hand-written 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 computer-aided verification 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
  • run-time 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 Botop-Butucaru. Models for mobile robots from continus to discrete spaces.
  • Ahmed Bouajjani. Verifying Event-Driven Asynchronous Programs against Concurrency.
  • Alessio Lomuscio. Verifying Fault-tolerance in Parameterised Multi-Agent Systems.
  • Ezio Bartocci. Monitoring Mobile and Spatially Distributed Cyber-Physical Systems.
  • Alexey Gotsman. Modular verification of consensus protocols.
  • Philippe Quéinnec. Describing asynchronous communications in distributed algorithms.
  • Tali Sznajder. Parameterized Verification of Algorithms for Oblivious Robots on a Ring.
  • Cezara Drăgoi. tba.
  • Thibaut Balabonski. Certified Gathering of Oblivious Mobile Robots.
  • Sylvain Conchon. Cubicle : a model checker for parameterized array-based transition systems


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 1st 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 2nd FRIDA workshop took place in Grenoble as part of FORTE’15. The 3rd FRIDA workshop was organized in Marrakech as part of NETYS’16.