Dagstuhl Seminar 23112
Unifying Formal Methods for Trustworthy Distributed Systems
( Mar 12 – Mar 15, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23112
Organizers
- Swen Jacobs (CISPA - Saarbrücken, DE)
- Kenneth McMillan (University of Texas - Austin, US)
- Roopsha Samanta (Purdue University - West Lafayette, US)
- Ilya Sergey (National University of Singapore, SG)
Contact
- Andreas Dolzmann (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Schedule
Dagstuhl Seminar 23112 Unifying Formal Methods for Trustworthy Distributed Systems took place on March 12-15, 2023 and had 25 participants: 9 female and 16 male, 22 from academia and 4 from industry, representing 9 different countries.
This was a short seminar spanning 2.5 days and included four one-hour keynotes, 16 regular and short (lightning) talks, as well as two two-hour whole-seminar plenary discussions. The keynote talks were given by
- Peter Müller (ETH Zurich) on Verified Secure Routing
- Ken McMillan (UT Austin) on Techniques for Decidable Verification
- Swen Jacobs (CISPA) on Parameterized Model Checking and Synthesis
- Murdoch Jamie Gabbay (Heriot-Watt University) on Semitopologies for Heterogeneous Consensus.
The abstracts of all talks appear in this seminar report, except for one of the keynotes and two impromptu talks for which we only give the titles here:
- „Taming Unbounded Distributed Systems with Modular, Bounded Verification“ by Roopsha Samanta (Purdue University), and
- „Pushing Formal Methods Tools to Industry“ by Mike Dodds (Galois).
The two plenary discussions that have taken place during the seminar were focusing on the topics of (1) performing comparative studies amongst different approaches for validating distributed systems and (2) grand challenges that call for joint efforts across different approaches and schools of thought in this area.
The outcome of the first discussion was an informal proposal on a „Distributed System Verification Competition“ - a community effort in the spirit of the famous „VerifyThis“ competition in software verification, which would offer, on a regular basis, a selection of micro-benchmarks and semi-artificial challenges in verification, validation, and bug-finding in distributed system, focusing on different aspects of safety, liveness and providing a landscape to showcase the recent advances in interactive or automated verification.
The second panel has concluded with several ideas of a large-scale verification/validation effort in distributed systems. The most viable option was suggested based on the topic of the first keynote talk on Verified Secure Routing, which is currently only partially achieved by a combination of two specific technologies and leaves a lot of room to improvement, both in terms of specification of the properties of interest (e.g., liveness) as well as for exploring possibilities for automating proofs as well as complementing sound verification methods with testing and dynamic analyses.
Given the short nature of this seminar, the social component of its program was limited to a dinner in local restaurant „Zum Schlossberg“, during which possibilities for collaboration have been discussed between the participants. As one outcome of this social interaction, possible internship opportunities in system verification were offered by one of the industry participants, with one of the junior participants currently considering taking them for the Summer 2024.
The seminar has generated several ideas for follow-up meetings. In particular, the following areas will likely benefit from more focused discussions and exchanges: (a) testing and dynamic validation of distributed systems; (b) addressing the challenge of so-called „latent proof“ (ignored abstraction gap) in automated verification, and (c) programming-language based techniques for implementing large-scale systems with a support for formal reasoning and verification.
Creative Commons BY 4.0
Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey
Distributed systems are challenging to develop and reason about. Unsurprisingly, there have been many efforts in formally specifying, modeling, and verifying distributed systems. A bird's eye view of this vast body of work reveals two primary sensibilities. The first is that of semi-automated or interactive deductive verification targeting structured programs and implementations, and focusing on simplifying the user's task of providing inductive invariants. The second is that of fully-automated model checking, targeting more abstract models of distributed systems, and focusing on extending the boundaries of decidability for the parameterized model checking problem. Regrettably, solution frameworks and results in deductive verification and parameterized model checking have largely evolved in isolation while targeting the same overall goal.
This Dagstuhl Seminar seeks to enable conversations and solutions cutting across the deductive verification and model checking communities, leveraging the complementary strengths of these approaches. In particular, the seminar will explore layered and compositional approaches for modeling and verification of industrial-scale distributed systems that lend themselves well to separation of verification tasks, and thereby the use of diverse proof methodologies.
We also recognize that formal methods education is an integral component of disseminating our research ideas for industrial-scale verification projects. Hence, another important objective of this seminar is to draw up a plan to train and teach relevant formal methods to students as well as industry partners.
We plan to make a publicly available website with the following information:
- A list of target verification problems developed collaboratively with our participants from industry (outlined before and finalized during the seminar)
- A summary of brainstorming sessions on unifying existing formal methods-based approaches for addressing the target problems
- Slides of all presentations
- A list of educational resources
We also expect to finalize initial plans for concrete collaborations across groups of participants. Finally, we hope to concretize plans for an annual summer school for training students and industry partners in the topics of this Dagstuhl Seminar.
Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey
- Laura Bocchi (University of Kent - Canterbury, GB) [dblp]
- Ahmed Bouajjani (Université Paris Cité, FR) [dblp]
- Andreea Costea (National University of Singapore, SG) [dblp]
- Mike Dodds (Galois - Portland, US) [dblp]
- Constantin Enea (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Javier Esparza (TU München, DE) [dblp]
- Murdoch Jamie Gabbay (Heriot-Watt University - Edinburgh, GB) [dblp]
- Swen Jacobs (CISPA - Saarbrücken, DE) [dblp]
- Gowtham Kaki (University of Colorado - Boulder, US) [dblp]
- Igor Konnov (Informal Systems - Wien, AT) [dblp]
- Burcu Kulahcioglu Ozkan (TU Delft, NL) [dblp]
- Lindsey Kuper (University of California - Santa Cruz, US) [dblp]
- Ori Lahav (Tel Aviv University, IL) [dblp]
- Marijana Lazic (TU München, DE) [dblp]
- Giuliano Losa (Stellar Development Foundation - San Francisco, US) [dblp]
- Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
- Kenneth McMillan (University of Texas - Austin, US) [dblp]
- Peter Müller (ETH Zürich, CH) [dblp]
- Kedar Namjoshi (Nokia Bell Labs - Murray Hill, US) [dblp]
- George Pîrlea (National University of Singapore, SG) [dblp]
- Roopsha Samanta (Purdue University - West Lafayette, US) [dblp]
- Ilya Sergey (National University of Singapore, SG) [dblp]
- Sharon Shoham Buchbinder (Tel Aviv University, IL) [dblp]
- Nobuko Yoshida (University of Oxford, GB) [dblp]
- Lenore D. Zuck (University of Illinois - Chicago, US) [dblp]
Classification
- Formal Languages and Automata Theory
- Logic in Computer Science
- Programming Languages
Keywords
- Industrial-Scale Distributed Systems
- Formal Verification
- Parameterized Model Checking
- Deductive Verification
- Compositional Reasoning
