Dagstuhl Seminar 13141
Formal Verification of Distributed Algorithms
( Apr 01 – Apr 05, 2013 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/13141
Organizers
- Bernadette Charron-Bost (Ecole Polytechnique - Palaiseau, FR)
- Stephan Merz (LORIA - Nancy, FR)
- Andrey Rybalchenko (TU München, DE)
- Josef Widder (TU Wien, AT)
Contact
- Annette Beyer (for administrative matters)
Schedule
While today’s society depends heavily on the correct functioning of distributed computing systems, the current approach to designing and implementing them is still error prone. We argue that this is because there is a methodological gap between the theory of distributed computing and the practice of designing and verifying the correctness of reliable distributed systems. We believe that there are two major reasons for this gap: On the one hand, distributed computing models are traditionally represented mainly in natural language, and algorithms are described in pseudo code. The classical approach to distributed algorithms is thus not very formal, and it is not always clear under which circumstances a given distributed algorithm actually is correct. On the other hand, distributed algorithms are designed to overcome non-determinism due to issues that are not within the control of the distributed algorithm, including the system’s timing behavior or faults of some components. Such issues lead to a huge executions space which is the major obstacle in applying verification tools to distributed algorithms.
We believe that researchers from distributed algorithms and formal verification should start working together to close the methodological gap. A big obstacle for common work is the lack of a universal model for distributed computing that allows expressing many distributed algorithms. Unlike sequential programs, whose semantics are well understood and closely follows the program text, the executions of distributed algorithms are to a large extent determined by the environment, including issues such as the distribution of processes, timing behavior, inter-process communication, and component faults. Models of distributed algorithms and systems embody different assumptions about how the environment behaves. These hypotheses are often left implicit but are of crucial importance for assessing the correctness of distributed algorithms. The seminar shall provide researchers in formal methods with an opportunity to learn more about the models underlying distributed algorithms, and find new exciting areas for developing and applying formal verification techniques.
In the area of sequential or synchronous parallel algorithms, high level of trust in correctness can be gained by the use of tools for formal verification such as static analysis, model checking or theorem proving. Such tools have been applied successfully in areas such as hardware design or device driver development. Hence, there exists a substantial amount of work on formal verification, but only relatively few specific distributed algorithms have been verified in specific models. We hope that researchers in distributed and dependable computing can learn more about the strengths and limitations of existing formal methods, and how these methods may help in their own work.
The seminar will contain tutorials on fundamentals of distributed computing, model checking, and semi-automated proofs. We will bring together experts from the fields related to this seminar topic to presentation their work and open questions. In addition, the program will contain ample room for lively discussion and debate on the issues raised.
While today's society depends heavily on the correct functioning of distributed computing systems, the current approach to designing and implementing them is still error prone. This is because there is a methodological gap between the theory of distributed computing and the practice of designing and verifying the correctness of reliable distributed systems.We believe that there are two major reasons for this gap: On the one hand, distributed computing models are traditionally represented mainly in natural language, and algorithms are described in pseudo code. The classical approach to distributed algorithms is thus informal, and it is not always clear under which circumstances a given distributed algorithm actually is correct. On the other hand, distributed algorithms are designed to overcome non-determinism due to issues that are not within the control of the distributed algorithm, including the system's timing behavior or faults of some components. Such issues lead to a huge executions space which is the major obstacle in applying verification tools to distributed algorithms.
The rationale behind our Dagstuhl seminar was that closing the methodological gap requires collaboration from researchers from distributed algorithms and formal verification. In order to spur the interaction between the communities, the program contained the following overview talks on the related subjects:
- Distributed algorithms: Eric Ruppert (York University)
- Semi-automated proofs: John Rushby (SRI)
- Parameterized model checking: Muralidhar Talupur (Intel)
In addition to the tutorials, we organized several open discussion rounds. The seminar participants identified modeling issues as a central question, which confirmed one of our motivation for the seminar, namely, the lack of a universal model for distributed algorithms. Hence, one of the discussion rounds was exclusively devoted to this topic. Unlike sequential programs, whose semantics is well understood and closely follows the program text, the executions of distributed algorithms are to a large extent determined by the environment, including issues such as the distribution of processes, timing behavior, inter-process communication, and component faults. Models of distributed algorithms and systems embody different assumptions about how the environment behaves. These hypotheses are often left implicit but are of crucial importance for assessing the correctness of distributed algorithms. The discussions during the seminar raised the awareness of these issue among the researchers, and showed that research in this area is a necessary first step towards a structured approach to formal verification of distributed algorithms. In addition to modeling, we discussed issues such as benchmarks, implementation of distributed algorithms, or application areas of distributed algorithms.
To round-off the technical program, we had several short presentations by participants who presented their past and current work in the intersection of formal methods and distributed algorithms, and a joint session with the other seminar going on concurrently at Dagstuhl on Correct and Efficient Accelerator Programming. The topics of the talks spanned large parts of the concerned areas, for instance, there were talks on model checking techniques such as partial order reductions or abstractions, and their applications to distributed algorithms; several talks focuses on proof assistants, and how they can be used to verify distributed algorithms; some talks considered concurrent systems, and some focused on transactional memory. The atmosphere during these sessions was very constructive, and the short talks were always followed by elaborate and insightful discussions.
Creative Commons BY 3.0 Unported license
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, and Josef Widder
- Béatrice Bérard (UPMC - Paris, FR) [dblp]
- Péter Bokor (ALTEN Engineering - Berlin, DE) [dblp]
- Borzoo Bonakdarpour (University of Waterloo, CA) [dblp]
- Pierre Castéran (University of Bordeaux, FR) [dblp]
- Bernadette Charron-Bost (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Marie Duflot (LORIA & INRIA Nancy, FR) [dblp]
- Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
- Matthias Függer (TU Wien, AT) [dblp]
- Alexey Gotsman (IMDEA Software - Madrid, ES) [dblp]
- Serge Haddad (ENS - Cachan, FR) [dblp]
- Gerwin Klein (Data61 / NICTA - Sydney, AU) [dblp]
- Igor Konnov (TU Wien, AT) [dblp]
- Fabrice Kordon (UPMC - Paris, FR) [dblp]
- Akash Lal (Microsoft Research India - Bangalore, IN) [dblp]
- Victor Luchangco (Oracle Corporation - Burlington, US) [dblp]
- Stephan Merz (LORIA - Nancy, FR) [dblp]
- Uwe Nestmann (TU Berlin, DE) [dblp]
- Thomas Nowak (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Eric Ruppert (York University - Toronto, CA) [dblp]
- John Rushby (SRI - Menlo Park, US) [dblp]
- Andrey Rybalchenko (TU München, DE) [dblp]
- André Schiper (EPFL - Lausanne, CH) [dblp]
- Klaus Schneider (TU Kaiserslautern, DE) [dblp]
- Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
- Wilfried Steiner (TTTech Computertechnik - Wien, AT) [dblp]
- Murali Talupur (Intel Corp. - Hillsboro, US) [dblp]
- Serdar Tasiran (Koc University - Istanbul, TR) [dblp]
- Helmut Veith (TU Wien, AT) [dblp]
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Jennifer L. Welch (Texas A&M University - College Station, US) [dblp]
- Josef Widder (TU Wien, AT) [dblp]
- Karsten Wolf (Universität Rostock, DE) [dblp]
Classification
- networks
- semantics / formal methods
- verification / logic
Keywords
- Distributed algorithms
- semi-automated proofs
- model checking
