https://www.dagstuhl.de/22492

04. – 09. Dezember 2022, Dagstuhl-Seminar 22492

Formal Methods and Distributed Computing: Stronger Together

Organisatoren

Hagit Attiya (Technion – Haifa, IL)
Constantin Enea (Ecole Polytechnique – Palaiseau, FR & CNRS – Palaiseau, FR)
Sergio Rajsbaum (National Autonomous University of Mexico, MX)
Ana Sokolova (Universität Salzburg, AT)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Marsha Kleinbauer zu wissenschaftlichen Fragen

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl-Seminar Wiki
Programm des Dagstuhl-Seminars [pdf] (Aktualisieren)

(Zum Einloggen bitte persönliche DOOR-Zugangsdaten verwenden)

Motivation

Distributed applications represent nowadays a significant part of our everyday life. To mention just a few examples, 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 increasingly deployed at large scale, they have to be reliable and robust, satisfying stringent correctness criteria. This is the point where a strong interaction of formal methods and of distributed computing becomes a necessity.

The goal of this Dagstuhl Seminar is to achieve a synergy by bringing together researchers working on applying formal methods for concurrent programs and distributed systems, and researchers from distributed computing. Both communities have a deep understanding of distributed computation, but from two different perspectives. Historically, these communities have common roots, but since more than two decades they evolved independently. The resulting gap slows down progress in both fields, and limits the applicability of the results obtained in each field, as each one develops its own techniques separately. The seminar addresses several topics that bridge the two research fields, and that have high potential to stimulate the development of the other area:

  • concurrent data structures and transactions: Modern multicore architectures enable large performance boosts by executing a number of threads in parallel, which however, poses considerable challenges in maintaining correctness of shared data structures and thread synchronization. These challenges have been addressed using various paradigms like lock-free programming or transactional memory. However, turning these concepts into efficient programming support remains a big challenge, and formal methods may offer new ideas in this direction.
  • formal approaches to large-scale replication: Current computing systems are increasingly large-scale distributed systems, for example, distributed databases, distributed ledgers (Blockchains) and key-value stores. At the heart of these systems are fundamental trade-offs between data consistency, availability, and the ability to tolerate failures. A formal approach to studying these issues will provide a common ground for the design, verification, analysis, implementation and use of these systems.
  • distributed algorithms for verification: Reasoning about concurrent/distributed software is notoriously difficult due to the inherent non-determinism in its semantics. The different processes in a concurrent program can interleave in many different ways which leads to an enormous number of possible executions. Algorithmic methods are necessary to mitigate the difficulty of reasoning about this huge space of executions, and scalable distributed algorithms may be the answer for the future. These methods can manifest in various forms, e.g., automated testing, deductive verification, model checking, and have led to important results in many timely contexts. Performing verification in a distributed fashion is a particularly promising new direction of research.

We believe that the impact of all the areas above on a rigorous development of distributed applications can be enhanced by fostering direct interactions between researchers from (automated) formal methods and from distributed computing through this Dagstuhl Seminar.

Motivation text license
  Creative Commons BY 4.0
  Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

Related Dagstuhl-Seminar

Classification

  • Distributed / Parallel / And Cluster Computing
  • Logic In Computer Science
  • Other Computer Science

Keywords

  • Distributed algorithms
  • Automated verification and reasoning
  • Concurrent data structures and transactions
  • Large-scale replication

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).

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.

Publikationen

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