The 6th Workshop on Formal Reasoning in Distributed Algorithms
Co-located with DISC 2019 (Budapest, Hungary) on October 18, 2019
|Workshop day||October 18, 2019|
If you like to give a talk at FRIDA, but have not been invited yet, send the talk title and a short abstract (max. one page) to the organizers. Presentation of papers published elsewhere is acceptable and encouraged, provided that the material fits the scope of the workshop. There will be no formal workshop proceedings — therefore, the work will be considered “unpublished”.
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 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 FRIDA workshop are:
- models for distributed algorithms
- model checking
- proof assistants & theorem proving
- parameterized model checking
- integration of different verification techniques
- distributed algorithm theory
- benchmark distributed algorithms
- fault tolerance
- automated code generation for distributed systems
- run-time verification of distributed systems
- Swen Jacobs (CISPA Helmholtz Center for Information Security)
- Igor Konnov (INRIA Nancy & LORIA)
- Stephan Merz (INRIA Nancy & LORIA)
- Josef Widder (TU Wien)
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 2ndFRIDA 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).