Search Results

Documents authored by Jacobs, Swen

Document
DOI: 10.4230/DagRep.13.3.32
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)

Authors: Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey

Published in: Dagstuhl Reports, Volume 13, Issue 3 (2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DagRep.13.3.32},
  URN =		{urn:nbn:de:0030-drops-192278},
  doi =		{10.4230/DagRep.13.3.32},
  annote =	{Keywords: Deductive Verification, Distributed Algorithms, Formal Verification, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.29
Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings

Authors: Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.
Cite as

Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour. Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{mirzaie_et_al:LIPIcs.OPODIS.2018.29,
  author =	{Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo},
  title =	{{Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.29},
  URN =		{urn:nbn:de:0030-drops-100896},
  doi =		{10.4230/LIPIcs.OPODIS.2018.29},
  annote =	{Keywords: Parameterized synthesis, Self-stabilization, Formal methods}
}
Document
DOI: 10.4230/DagSemProc.07401.6
Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

Authors: Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

Abstract
Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions of literals in a background theory. This can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We present some new results on hierarchical and modular reasoning in complex theories, as well as several examples of application domains in which efficient reasoning is possible. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of local theory extension.
Cite as

Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local Theory Extensions, Hierarchical Reasoning and Applications to Verification. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{sofroniestokkermans_et_al:DagSemProc.07401.6,
  author =	{Sofronie-Stokkermans, Viorica and Ihlemann, Carsten and Jacobs, Swen},
  title =	{{Local Theory Extensions, Hierarchical Reasoning and Applications to Verification}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.6},
  URN =		{urn:nbn:de:0030-drops-12507},
  doi =		{10.4230/DagSemProc.07401.6},
  annote =	{Keywords: Automated reasoning, Combinations of decision procedures, Verification}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact