Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)

Authors Swen Jacobs, Kenneth McMillan, Roopsha Samanta, Ilya Sergey and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.13.3.32.pdf
  • Filesize: 2.26 MB
  • 17 pages

Document Identifiers

Author Details

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
and all authors of the abstracts in this report

Cite AsGet BibTex

Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey. Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). In Dagstuhl Reports, Volume 13, Issue 3, pp. 32-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DagRep.13.3.32

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.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed algorithms
  • Theory of computation → Concurrency
  • Theory of computation → Program verification
Keywords
  • Deductive Verification
  • Distributed Algorithms
  • Formal Verification
  • Model Checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail