http://www.dagstuhl.de/18211

May 21 – 25 , 2018, Dagstuhl Seminar 18211

Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance

Organizers

Javier Esparza (TU München, DE)
Pierre Fraigniaud (University Paris-Diderot, FR)
Anca Muscholl (University of Bordeaux, FR)
Sergio Rajsbaum (National Autonomous University of Mexico, MX)

For support, please contact

Jutka Gasiorowski for administrative matters

Andreas Dolzmann for scientific matters

Documents

Dagstuhl Seminar Schedule (Upload here)

(Use seminar number and access code to log in)

Motivation

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.

License
  Creative Commons BY 3.0 DE
  Javier Esparza, Pierre Fraigniaud, Anca Muscholl, and Sergio Rajsbaum

Classification

  • Data Structures / Algorithms / Complexity
  • Verification / Logic

Keywords

  • Distributed computing
  • Formal verification
  • Distributed systems

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support