Search Results

Documents authored by Dragoi, Cezara

Found 2 Possible Name Variants:

Drăgoi, Cezara

Document
DOI: 10.4230/LIPIcs.SNAPL.2015.90
The Need for Language Support for Fault-Tolerant Distributed Systems

Authors: Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.
Cite as

Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. The Need for Language Support for Fault-Tolerant Distributed Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 90-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dragoi_et_al:LIPIcs.SNAPL.2015.90,
  author =	{Dragoi, Cezara and Henzinger, Thomas A. and Zufferey, Damien},
  title =	{{The Need for Language Support for Fault-Tolerant Distributed Systems}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{90--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.90},
  URN =		{urn:nbn:de:0030-drops-50192},
  doi =		{10.4230/LIPIcs.SNAPL.2015.90},
  annote =	{Keywords: Programming language, Fault-tolerant distributed algorithms, Automated verification}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2356
Rewriting Systems over Nested Data Words

Authors: Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract
We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.
Cite as

Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu. Rewriting Systems over Nested Data Words. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 70-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:OASIcs:2009:DROPS.MEMICS.2009.2356,
  author =	{Bouajjani, Ahmed and Dr\u{a}goi, Cezara and Jurski, Yan and Sighireanu, Mihaela},
  title =	{{Rewriting Systems over Nested Data Words}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{70--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2356},
  URN =		{urn:nbn:de:0030-drops-23567},
  doi =		{10.4230/DROPS.MEMICS.2009.2356},
  annote =	{Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking}
}

Dragoi, Cezara

Document
DOI: 10.4230/LIPIcs.SNAPL.2015.90
The Need for Language Support for Fault-Tolerant Distributed Systems

Authors: Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.
Cite as

Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. The Need for Language Support for Fault-Tolerant Distributed Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 90-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dragoi_et_al:LIPIcs.SNAPL.2015.90,
  author =	{Dragoi, Cezara and Henzinger, Thomas A. and Zufferey, Damien},
  title =	{{The Need for Language Support for Fault-Tolerant Distributed Systems}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{90--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.90},
  URN =		{urn:nbn:de:0030-drops-50192},
  doi =		{10.4230/LIPIcs.SNAPL.2015.90},
  annote =	{Keywords: Programming language, Fault-tolerant distributed algorithms, Automated verification}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2356
Rewriting Systems over Nested Data Words

Authors: Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract
We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.
Cite as

Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu. Rewriting Systems over Nested Data Words. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 70-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:OASIcs:2009:DROPS.MEMICS.2009.2356,
  author =	{Bouajjani, Ahmed and Dr\u{a}goi, Cezara and Jurski, Yan and Sighireanu, Mihaela},
  title =	{{Rewriting Systems over Nested Data Words}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{70--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2356},
  URN =		{urn:nbn:de:0030-drops-23567},
  doi =		{10.4230/DROPS.MEMICS.2009.2356},
  annote =	{Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking}
}
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 About DROPS Imprint Privacy Contact