Search Results

Documents authored by Lazic, Marijana

Found 2 Possible Name Variants:

Lazic, Marijana

Document
DOI: 10.4230/LIPIcs.DISC.2022.10
Holistic Verification of Blockchain Consensus

Authors: Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)

Abstract
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in various blockchain consensus algorithms [Pierre Tholoniat and Vincent Gramoli, 2019]. Paradoxically, until now, no blockchain consensus has been holistically verified. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [Tyler Crain et al., 2021], for any number n of processes and any number f < n/3 of Byzantine processes. We decompose directly the algorithm pseudocode in two parts - an inner broadcast algorithm and an outer decision algorithm - each modelled as a threshold automaton [Igor Konnov et al., 2017], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its proven properties. Doing so, we formally verify, for any parameter, not only the safety properties of the Red Belly Blockchain consensus but also its liveness in less than 70 seconds.
Cite as

Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder. Holistic Verification of Blockchain Consensus. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.DISC.2022.10,
  author =	{Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazi\'{c}, Marijana and Tholoniat, Pierre and Widder, Josef},
  title =	{{Holistic Verification of Blockchain Consensus}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.10},
  URN =		{urn:nbn:de:0030-drops-172019},
  doi =		{10.4230/LIPIcs.DISC.2022.10},
  annote =	{Keywords: Model checking, automata, logic, byzantine failure}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.21
Wait-Free Solvability of Equality Negation Tasks

Authors: Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k<l, indicating when the cardinality of the set of inputs becomes "small" or "large", respectively. We study the solvability of this task depending on those two parameters. First, we show that the task is solvable whenever k+2 <= l. For the remaining cases (l = k+1), we use various combinatorial topology techniques to obtain two impossibility results: the task is unsolvable if either k <= n/2 or n-k is odd. The remaining cases are still open.
Cite as

Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum. Wait-Free Solvability of Equality Negation Tasks. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2019.21,
  author =	{Goubault, \'{E}ric and Lazi\'{c}, Marijana and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{Wait-Free Solvability of Equality Negation Tasks}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.21},
  URN =		{urn:nbn:de:0030-drops-113288},
  doi =		{10.4230/LIPIcs.DISC.2019.21},
  annote =	{Keywords: Equality negation, distributed computability, combinatorial topology}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.33
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Authors: Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.
Cite as

Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2019.33,
  author =	{Bertrand, Nathalie and Konnov, Igor and Lazi\'{c}, Marijana and Widder, Josef},
  title =	{{Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.33},
  URN =		{urn:nbn:de:0030-drops-109358},
  doi =		{10.4230/LIPIcs.CONCUR.2019.33},
  annote =	{Keywords: threshold automata, counter systems, parameterized verification, randomized distributed algorithms, Byzantine faults}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2017.32
Synthesis of Distributed Algorithms with Parameterized Threshold Guards

Authors: Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
Fault-tolerant distributed algorithms are notoriously hard to get right. In this paper we introduce an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts. Fault-tolerant distributed algorithms are typically parameterized, that is, they are designed to work for any number n of processes and any number t of faults, provided some resilience condition holds; e.g., n > 3t. In this paper we automatically synthesize distributed algorithms that work for all parameter values that satisfy the resilience condition. We focus on threshold- guarded distributed algorithms, where actions are taken only if a sufficiently large number of messages is received, e.g., more than t or n/2. Both expressions can be derived by choosing the right values for the coefficients a, b, and c, in the sketch of a threshold a·n+b·t+c. Our method takes as input a sketch of an asynchronous threshold-based fault-tolerant distributed algorithm — where the guards are missing exact coefficients—and then iteratively picks the values for the coefficients. Our approach combines recent progress in parameterized model checking of distributed algo- rithms with counterexample-guided synthesis. Besides theoretical results on termination of the synthesis procedure, we experimentally evaluate our method and show that it can synthesize sev- eral distributed algorithms from the literature, e.g., Byzantine reliable broadcast and Byzantine one-step consensus. In addition, for several new variations of safety and liveness specifications, our tool generates new distributed algorithms.
Cite as

Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem. Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lazic_et_al:LIPIcs.OPODIS.2017.32,
  author =	{Lazic, Marijana and Konnov, Igor and Widder, Josef and Bloem, Roderick},
  title =	{{Synthesis of Distributed Algorithms with Parameterized Threshold Guards}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.32},
  URN =		{urn:nbn:de:0030-drops-86359},
  doi =		{10.4230/LIPIcs.OPODIS.2017.32},
  annote =	{Keywords: fault-tolerant distributed algorithms, byzantine faults, parameterized model checking, program synthesis}
}

Lazić, Marijana

Document
DOI: 10.4230/LIPIcs.DISC.2022.10
Holistic Verification of Blockchain Consensus

Authors: Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)

Abstract
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in various blockchain consensus algorithms [Pierre Tholoniat and Vincent Gramoli, 2019]. Paradoxically, until now, no blockchain consensus has been holistically verified. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [Tyler Crain et al., 2021], for any number n of processes and any number f < n/3 of Byzantine processes. We decompose directly the algorithm pseudocode in two parts - an inner broadcast algorithm and an outer decision algorithm - each modelled as a threshold automaton [Igor Konnov et al., 2017], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its proven properties. Doing so, we formally verify, for any parameter, not only the safety properties of the Red Belly Blockchain consensus but also its liveness in less than 70 seconds.
Cite as

Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, and Josef Widder. Holistic Verification of Blockchain Consensus. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.DISC.2022.10,
  author =	{Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazi\'{c}, Marijana and Tholoniat, Pierre and Widder, Josef},
  title =	{{Holistic Verification of Blockchain Consensus}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.10},
  URN =		{urn:nbn:de:0030-drops-172019},
  doi =		{10.4230/LIPIcs.DISC.2022.10},
  annote =	{Keywords: Model checking, automata, logic, byzantine failure}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.21
Wait-Free Solvability of Equality Negation Tasks

Authors: Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k<l, indicating when the cardinality of the set of inputs becomes "small" or "large", respectively. We study the solvability of this task depending on those two parameters. First, we show that the task is solvable whenever k+2 <= l. For the remaining cases (l = k+1), we use various combinatorial topology techniques to obtain two impossibility results: the task is unsolvable if either k <= n/2 or n-k is odd. The remaining cases are still open.
Cite as

Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum. Wait-Free Solvability of Equality Negation Tasks. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2019.21,
  author =	{Goubault, \'{E}ric and Lazi\'{c}, Marijana and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{Wait-Free Solvability of Equality Negation Tasks}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.21},
  URN =		{urn:nbn:de:0030-drops-113288},
  doi =		{10.4230/LIPIcs.DISC.2019.21},
  annote =	{Keywords: Equality negation, distributed computability, combinatorial topology}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.33
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Authors: Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.
Cite as

Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2019.33,
  author =	{Bertrand, Nathalie and Konnov, Igor and Lazi\'{c}, Marijana and Widder, Josef},
  title =	{{Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.33},
  URN =		{urn:nbn:de:0030-drops-109358},
  doi =		{10.4230/LIPIcs.CONCUR.2019.33},
  annote =	{Keywords: threshold automata, counter systems, parameterized verification, randomized distributed algorithms, Byzantine faults}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2017.32
Synthesis of Distributed Algorithms with Parameterized Threshold Guards

Authors: Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
Fault-tolerant distributed algorithms are notoriously hard to get right. In this paper we introduce an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts. Fault-tolerant distributed algorithms are typically parameterized, that is, they are designed to work for any number n of processes and any number t of faults, provided some resilience condition holds; e.g., n > 3t. In this paper we automatically synthesize distributed algorithms that work for all parameter values that satisfy the resilience condition. We focus on threshold- guarded distributed algorithms, where actions are taken only if a sufficiently large number of messages is received, e.g., more than t or n/2. Both expressions can be derived by choosing the right values for the coefficients a, b, and c, in the sketch of a threshold a·n+b·t+c. Our method takes as input a sketch of an asynchronous threshold-based fault-tolerant distributed algorithm — where the guards are missing exact coefficients—and then iteratively picks the values for the coefficients. Our approach combines recent progress in parameterized model checking of distributed algo- rithms with counterexample-guided synthesis. Besides theoretical results on termination of the synthesis procedure, we experimentally evaluate our method and show that it can synthesize sev- eral distributed algorithms from the literature, e.g., Byzantine reliable broadcast and Byzantine one-step consensus. In addition, for several new variations of safety and liveness specifications, our tool generates new distributed algorithms.
Cite as

Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem. Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lazic_et_al:LIPIcs.OPODIS.2017.32,
  author =	{Lazic, Marijana and Konnov, Igor and Widder, Josef and Bloem, Roderick},
  title =	{{Synthesis of Distributed Algorithms with Parameterized Threshold Guards}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.32},
  URN =		{urn:nbn:de:0030-drops-86359},
  doi =		{10.4230/LIPIcs.OPODIS.2017.32},
  annote =	{Keywords: fault-tolerant distributed algorithms, byzantine faults, parameterized model checking, program synthesis}
}
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