2 Search Results for "Samanta, Roopsha"

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-dev.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.FSTTCS.2014.431
Lipschitz Robustness of Finite-state Transducers

Authors: Thomas A. Henzinger, Jan Otop, and Roopsha Samanta

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using set-similarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.
Cite as

Thomas A. Henzinger, Jan Otop, and Roopsha Samanta. Lipschitz Robustness of Finite-state Transducers. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 431-443, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.FSTTCS.2014.431,
  author =	{Henzinger, Thomas A. and Otop, Jan and Samanta, Roopsha},
  title =	{{Lipschitz Robustness of Finite-state Transducers}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{431--443},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.431},
  URN =		{urn:nbn:de:0030-drops-48614},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.431},
  annote =	{Keywords: Robustness, Transducers, Weighted Automata}
}
  • Refine by Author
  • 2 Samanta, Roopsha
  • 1 Henzinger, Thomas A.
  • 1 Jacobs, Swen
  • 1 McMillan, Kenneth
  • 1 Otop, Jan
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Distributed algorithms
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Deductive Verification
  • 1 Distributed Algorithms
  • 1 Formal Verification
  • 1 Model Checking
  • 1 Robustness
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2014
  • 1 2023

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