Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Innerhalb dieser Seite:
Externe Seiten:
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp

Dagstuhl-Seminar 18211

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

( 21. May – 25. May, 2018 )

(zum Vergrößern in der Bildmitte klicken)

Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:




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.
Copyright Javier Esparza, Pierre Fraigniaud, Anca Muscholl, and Sergio Rajsbaum

  • Paul C. Attie (American University of Beirut, LB) [dblp]
  • Hagit Attiya (Technion - Haifa, IL) [dblp]
  • A. R. Balasubramanian (Chennai Mathematical Institute, IN) [dblp]
  • Michael Blondin (TU München, DE) [dblp]
  • Benedikt Bollig (ENS - Cachan, FR) [dblp]
  • Borzoo Bonakdarpour (McMaster University - Hamilton, CA) [dblp]
  • Ahmed Bouajjani (University Paris-Diderot, FR) [dblp]
  • Dan Brownstein (Ben Gurion University - Beer Sheva, IL) [dblp]
  • Keren Censor-Hillel (Technion - Haifa, IL) [dblp]
  • Aiswarya Cyriac (Chennai Mathematical Institute, IN) [dblp]
  • Giorgio Delzanno (University of Genova, IT) [dblp]
  • Cezara Dragoi (ENS - Paris, FR) [dblp]
  • Jo Ebergen (Oracle Labs - Redwood Shores, US) [dblp]
  • Yuval Emek (Technion - Haifa, IL) [dblp]
  • Constantin Enea (University Paris-Diderot, FR) [dblp]
  • Javier Esparza (TU München, DE) [dblp]
  • Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
  • Marie Fortin (ENS - Cachan, FR) [dblp]
  • Pierre Fraigniaud (University Paris-Diderot and CNRS, FR) [dblp]
  • Matthias Függer (ENS - Cachan, FR) [dblp]
  • Paul Gastin (ENS - Cachan, FR) [dblp]
  • Swen Jacobs (Universität des Saarlandes, DE) [dblp]
  • Igor Konnov (INRIA Nancy - Grand Est, FR) [dblp]
  • Sandeep Kulkarni (Michigan State University - East Lansing, US) [dblp]
  • Marijana Lazic (TU Wien, AT) [dblp]
  • Jérémy Ledent (Ecole Polytechnique - Palaiseau, FR) [dblp]
  • Martin Leucker (Universität Lübeck, DE) [dblp]
  • Stephan Merz (INRIA Nancy - Grand Est, FR) [dblp]
  • Roland Meyer (TU Braunschweig, DE) [dblp]
  • Yoram Moses (Technion - Haifa, IL) [dblp]
  • Anca Muscholl (University of Bordeaux, FR) [dblp]
  • Rotem Oshman (Tel Aviv University, IL) [dblp]
  • Mor Perry (Tel Aviv University, IL) [dblp]
  • Sergio Rajsbaum (National Autonomous University of Mexico, MX) [dblp]
  • David A. Rosenblueth (Universidad Nacional Autonoma - Mexico, MX) [dblp]
  • Arnaud Sangnier (University Paris-Diderot, FR) [dblp]
  • Ana Sokolova (Universität Salzburg, AT) [dblp]
  • Paola Spoletini (Kennesaw State University - Marietta, US) [dblp]
  • Corentin Travers (University of Bordeaux, FR) [dblp]
  • Igor Walukiewicz (University of Bordeaux, FR) [dblp]
  • Philipp Woelfel (University of Calgary, CA) [dblp]

Verwandte Seminare
  • Dagstuhl-Seminar 22492: Formal Methods and Distributed Computing: Stronger Together (2022-12-04 - 2022-12-09) (Details)

  • data structures / algorithms / complexity
  • verification / logic

  • distributed computing
  • formal verification
  • distributed systems