License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.13.3.32
URN: urn:nbn:de:0030-drops-192278
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19227/
Jacobs, Swen ;
McMillan, Kenneth ;
Samanta, Roopsha ;
Sergey, Ilya
Weitere Beteiligte (Hrsg. etc.): Swen Jacobs and Kenneth McMillan and Roopsha Samanta and Ilya Sergey
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23112 "Unifying Formal Methods for Trustworthy Distributed Systems".
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 seminar aimed at enabling conversations and solutions cutting across the deductive verification and model checking communities, leveraging the complementary strengths of these approaches. In particular, we explored 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.
BibTeX - Entry
@Article{jacobs_et_al:DagRep.13.3.32,
author = {Jacobs, Swen and McMillan, Kenneth and Samanta, Roopsha and Sergey, Ilya},
title = {{Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)}},
pages = {32--48},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2023},
volume = {13},
number = {3},
editor = {Jacobs, Swen and McMillan, Kenneth and Samanta, Roopsha and Sergey, Ilya},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19227},
URN = {urn:nbn:de:0030-drops-192278},
doi = {10.4230/DagRep.13.3.32},
annote = {Keywords: Deductive Verification, Distributed Algorithms, Formal Verification, Model Checking}
}
|
Keywords: |
|
Deductive Verification, Distributed Algorithms, Formal Verification, Model Checking |
|
Collection: |
|
DagRep, Volume 13, Issue 3 |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
16.10.2023 |
