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 22492

Formal Methods and Distributed Computing: Stronger Together

( Dec 04 – Dec 09, 2022 )

(Click in the middle of the image to enlarge)

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

Organizers

Contact


Schedule

Summary

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 was 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 addressed 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.

The impact of all the areas above on a rigorous development of distributed applications was enhanced by fostering direct interactions between researchers from (automated) formal methods and from distributed computing.

Copyright Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

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.

Copyright Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

Participants
  • Hagit Attiya (Technion - Haifa, IL) [dblp]
  • Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
  • Nathalie Bertrand (INRIA - Rennes, FR) [dblp]
  • Raven Beutner (CISPA - Saarbrücken, DE)
  • Annette Bieniusa (TU Kaiserslautern, DE) [dblp]
  • Ahmed Bouajjani (Université Paris Cité, FR) [dblp]
  • Manuel Bravo (Informal Systems - Madrid, ES) [dblp]
  • Armando Castaneda (National Autonomous University of Mexico, MX) [dblp]
  • Gregory Chockler (University of Surrey - Guildford, GB) [dblp]
  • Constantin Enea (Ecole Polytechnique - Palaiseau, FR & CNRS - Palaiseau, FR) [dblp]
  • Bernd Finkbeiner (CISPA - Saarbrücken, DE) [dblp]
  • Pierre Fraigniaud (Université de Paris, FR & CNRS, Paris, FR) [dblp]
  • Alexey Gotsman (IMDEA Software Institute - Madrid, ES) [dblp]
  • Maurice Herlihy (Brown University - Providence, US) [dblp]
  • Burcu Kulahcioglu Ozkan (TU Delft, NL) [dblp]
  • Sandeep Kulkarni (Michigan State University - East Lansing, US) [dblp]
  • Petr Kuznetsov (Telecom Paris, FR) [dblp]
  • Ori Lahav (Tel Aviv University, IL) [dblp]
  • Giuliano Losa (Stellar Development Foundation - San Francisco, US) [dblp]
  • Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Stephan Merz (INRIA Nancy - Grand Est, FR) [dblp]
  • Yoram Moses (Technion - Haifa, IL) [dblp]
  • Rotem Oshman (Tel Aviv University, IL) [dblp]
  • Azalea Raad (Imperial College London, GB) [dblp]
  • Sergio Rajsbaum (National Autonomous University of Mexico, MX) [dblp]
  • Ana Sokolova (Universität Salzburg, AT) [dblp]
  • Serdar Tasiran (Amazon Web Services - New York City, US) [dblp]
  • Viktor Vafeiadis (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Jennifer L. Welch (Texas A&M University - College Station, US) [dblp]
  • Thomas Wies (New York University, US) [dblp]
  • Philipp Woelfel (University of Calgary, CA) [dblp]

Related Seminars
  • Dagstuhl Seminar 18211: Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance (2018-05-21 - 2018-05-25) (Details)

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