TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 18211

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

( May 21 – May 25, 2018 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/18211

Organizers

Contact


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

Participants
  • 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]

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

Classification
  • data structures / algorithms / complexity
  • verification / logic

Keywords
  • distributed computing
  • formal verification
  • distributed systems