Distributed applications represent a significant part of our everyday life. Typically, our personal data are stored on remote distributed servers, data management relies on remote applications reachable via smartphones or tablets, data-intensive computations are performed on computer clusters, etc. Since distributed applications are deployed at increasingly large scale, they have to be reliable and robust, satisfying stringent correctness criteria. This is the point where a strong interaction between formal methods and distributed computing becomes a necessity.

The goal of this Dagstuhl Seminar is to bring together researchers working on the verification of concurrent programs and distributed systems, and researchers from distributed computing. Both communities have deep understanding of distributed computation, but from two different perspectives. Historically, these communities had common roots. However, since more than two decades, they tend to evolve independently. The seminar addresses several topics that can be viewed as bridges between the two aforementioned research fields, with potential fruitful co-developments:

1. Distributed runtime verification. Runtime verification is an appealing alternative method to traditional exhaustive exploration, positioned in between testing and model-checking. Designing distributed monitoring techniques is far more challenging than sequential monitoring, as the monitoring information has to be computed by a distributed algorithm, using only the communication means provided by the execution of the monitored program.
2. Distributed synthesis and control. Programs are seldom correct. For distributed programs, errors are even more frequent. Error recovery at runtime is an appealing alternative to correcting the program off-line. Failure monitoring provides information about the causes of failures, advising of possible repairs, including useful information in the presence of several alternative algorithms available for different operation modes.
3. Concurrent data structures and transactions. Modern multicore architectures enable the parallel execution of a large number of threads. The price to pay is to maintain the correctness of shared data-structures, and to enable thread synchronization. Transactional memory (TM) provides a high-level non-blocking synchronization mechanism. However, turning TM into efficient programming support remains a challenge.
4. Parameterized verification. Parameterized verification applies to the settings where the size of the system is unknown, and some property needs to be proven independently of the system size. This is a typical situation for distributed algorithms, where the correctness needs to be asserted for any number of participants.
5. Distributed decision. Distributed decision is a recent field of investigation within distributed computing, developed under different forms, including mechanisms for the design of self-* distributed algorithms, with applications to fault-tolerant computing, complexity and computability theory, property testing, etc. In contrast to formal verification, distributed decision puts emphasis on the design of algorithms for deciding the correctness of specific predicates (e.g., consensus, MST, etc.). To our knowledge, it is not known whether the field can be generalized to tackle larger classes of system predicates, and whether they can be adapted to automatic verification.

Creative Commons BY 3.0 DE

Javier Esparza, Pierre Fraigniaud, Anca Muscholl, and Sergio Rajsbaum