The 11th Workshop on Formal Reasoning in Distributed Algorithms

Date: Tuesday July 23rd, 2024

Location: Montreal, Canada

The workshop is organized as part of CAV 2024.

Speakers

If you would like to participate as a speaker, send an abstract by May 25th, 2024 to Swen Jacobs and Giuliano Losa. We welcome talks on recent published or unpublished research as well as new and exploratory ideas. See below for the topics of interest.

Description

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

• Swen Jacobs
• Giuliano Losa

With support of

• Stephan Merz
• Marijana Lazić
• Igor Konnov
• Joseph Widder

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 FRIDA workshop then took place every year since 2014.

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 online workshops at QONFEST 2020 and DISC 2021, respectively. FRIDA 2022 was organized with FLoC 2022 and took place in Haifa. FRIDA 2023 took place in L’Aquila, Italy, along with DISC 2024.