Formal Reasoning in Distributed Algorithms (FRIDA 2017)
October 20, 2017
Satellite workshop of DISC 2017 (Vienna, Austria)
|Workshop date||October 20, 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 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
- distributed algorithm theory
- benchmark distributed algorithms
- fault tolerance
- automated code generation for distributed systems
- run-time verification of distributed systems
- Swen Jacobs (Saarland University)
- Igor Konnov (TU Wien)
- 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 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.