Dagstuhl Seminar 23112
Unifying Formal Methods for Trustworthy Distributed Systems
( Mar 12 – Mar 15, 2023 )
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)
Dagstuhl Reports
As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.
- Upload (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
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.
Creative Commons BY 4.0
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
