Name
Abstract | ||
|---|---|---|
We present a fault-tolerant ordered broadcast service that is correct-by-construction. Our broadcast service allows for diversity in space, whereby the participants in the broadcast protocol run different code, as well as in time, whereby the protocol itself is changed periodically. We use the Nuprl proof assistant to specify the service, prove correctness, and synthesize the code. The paper includes initial performance results. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/ICNP.2012.6459943 | Network Protocols |
Keywords | Field | DocType |
nuprl proof assistant,different code,correct-by-construction broadcast service,broadcast service,initial performance result,broadcast protocol,protocols,formal verification,fault tolerance,broadcasting,formal specification | Broadcasting,Computer science,Correctness,Nuprl,Computer network,AC power,Formal specification,Fault tolerance,Formal verification,Proof assistant,Distributed computing | Conference |
ISSN | ISBN | Citations |
1092-1648 | 978-1-4673-2446-5 | 2 |
PageRank | References | Authors |
0.36 | 17 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Rahli | 1 | 43 | 9.21 |
| Nicolas Schiper | 2 | 173 | 10.18 |
| Robbert van Renesse | 3 | 4018 | 507.30 |
| M. Bickford | 4 | 101 | 8.60 |
| Robert L. Constable | 5 | 778 | 242.51 |