The 9th Workshop on Formal Reasoning in Distributed Algorithms

Date: August 11th 2022

The workshop is organized as part of FLoC 2022.

Regular registration is possible until July 20: https://www.floc2022.org/registration

News

  • July 7: added more speakers
  • June 13th: added first two speakers and registration link
  • May 23rd: website created!

Program

Confirmed speakers:

  • Hagit Attiya, Technion
  • Yoram Moses, Technion
  • Burcu Özkan, TU Delft
  • Constantin Enea, Ecole Polytechnique, LIX
  • Ilina Stoilkovska, AWS
  • Ori Lahav, Tel Aviv University
  • more to come soon!

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 FRIDA workshop include the following topics, as they apply to distributed algorithms and systems:

  • formal modeling
  • model checking
  • interactive theorem proving
  • parameterized model checking
  • integration of different verification techniques
  • benchmarking
  • synthesis
  • run-time verification
  • testing
  • invariant inference

Organizers

Main organizers

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. The 4th FRIDA workshop took place in Vienna as part of DISC 2017. The 5th FRIDA workshop was co-located with CAV 2018, which was held as part of the Federated Logic Conference (FLoC). The 6th workshop was co-located with DISC 2019 in Budapest, Hungary. Finally, FRIDA 2020 and FRIDA 2021 took place as an online workshops at QONFEST 2020 and DISC 2021, respectively.