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.

Creative Commons BY 4.0

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

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