FINAL PROGRAM [pdf]
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 include but are not limited to:
- models for distributed algorithms
- model checking
- proof assistants & theorem proving
- parameterized model checking
- integration of different verification techniques
- concurrency
- distributed algorithm theory
- case studies and benchmarks
- fault tolerance
- synthesis
- automated code generation for distributed systems
- run-time verification of distributed systems
Rationale
FRIDA is an informal follow-up workshop to a Dagstuhl seminar on formal verification of distributed algorithms (Formal Verification of Distributed Algorithms) held in 2013. In the next years, we continue to organize similar workshops in order to strengthen the collaboration between the concerned communities.
Invited talks
- Joe Halpern (Cornell University): Beyond Nash Equilibrium: Solution Concepts for the 21st Century.
- Alexander Shvartsman (University of Connecticut): Specifying, Reasoning About, Optimizing, and Implementing Atomic Data Services for Distributed Systems
Regular talks
- Laure Millet, Maria Gradinariu Potop-Butucaru, Nathalie Sznajder and Sebastien Tixeuil: On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering
- Joel Rybicki. Synthesizing self-stabilizing fault-tolerant algorithms.
- Mike Dodds, Andreas Haas and Christoph Kirsch: A Fast, Correct Time-Stamped Stack.
![[presentation]](http://forsyte.at/download/frida14/haas-frida14.svg){kind=link}
- Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters and Uwe Nestmann: Mechanical Verification of a Constructive Proof for FLP.
- Victor Altukhov, Eugene Chemeritskiy, Vladislav Podymov and Vladimir Zakharov: Models and techniques for verification of Software Defined Networks.
- Swen Jacobs: Parameterized Synthesis.
- Tobias Gawron-Deutsch: Verification and Validation Challenges in Smart Grids from the Industrial Perspective.
- Matthias Függer, Robert Najvirt, Thomas Nowak and Ulrich Schmid: Towards binary circuit models that faithfully reflect physical (un)solvability.
- Ana Sokolova: Concurrent Data Structures: Semantics and (Quantitative) Relaxation.
- Francesco Alberti, Silvio Ghilardi and Natasha Sharygina: Monotonic Abstraction Techniques: from Parametric to Software Model Checking.
- Cezara Dragoi, Josef Widder and Damien Zufferey: Round model for distributed algorithms: from verification to implementation.
- Cezara Dragoi, Thomas Henzinger, Helmut Veith, Josef Widder and Damien Zufferey: A Logic-based Framework for Verifying Consensus Algorithms.
- Nicolas Braud-Santoni and Swen Jacobs: Synthesis for Resilient Distributed Systems.
- Giorgio Delzanno and Michele Tatarek: Model Checking Distributed Consensus Algorithms.
Format
This two-day workshop will include invited talks, presentations of position papers, including work-in-progress and published work, and discussion periods. We are planning to collect the abstracts and the presentations for publication on the workshop site. In addition to some invited talks, the program will include short presentations of contributed position papers, a challenge problem session, and ample room for lively discussion and debate on the issues raised.
Important Dates
- Submission deadline: June 3, 2014
- Acceptance notification: June 5, 2014
- Workshop dates: July 23-24, 2014
Submission Instructions
We seek submissions reporting on theory, applications, case studies or open questions at the interface of formal methods and distributed algorithms. Contributions may range from extended abstracts of one or two pages to full papers of twenty pages, in Easychair format, and should be submitted as pdf files. Presentation of papers published elsewhere is acceptable and encouraged. There will be no formal workshop proceedings — therefore, the work will be considered “unpublished”. However, accepted contributions will be made accessible from the Workshop Web page.
Organization
- Borzoo Bonakdarpour (University of Waterloo) - chair
- Igor Konnov (Vienna University of Technology) - chair
- Stephan Merz (INRIA Nancy & LORIA) - chair
- Josef Widder (TU Wien) - chair
Sponsors
We are grateful to RiSE and Siemens for the sponsor support.
