http://www.dagstuhl.de/18211

21. – 25. Mai 2018, Dagstuhl Seminar 18211

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

Organisatoren

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)

Auskunft zu diesem Dagstuhl Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Andreas Dolzmann zu wissenschaftlichen Fragen

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

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.