Name
Abstract | ||
|---|---|---|
Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized model for both CAN and broadcast protocols over those networks. We demonstrate that our approach is practical by identifying sufficient conditions for a protocol to be correct and efficient. We also prove the existence of a protocol verifying those properties. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-37057-1_20 | FASE |
Keywords | Field | DocType |
functional correctness,algorithms run,p2p system,intimidating task,content addressable network,mechanized model,formal reasoning,broadcast algorithm,right level,broadcast protocol,theorem proving,can | Broadcast algorithm,Broadcasting,Formal reasoning,Programming language,Abstraction,Computer science,Content addressable network,Correctness,Automated theorem proving,Theoretical computer science | Conference |
Volume | ISSN | Citations |
7793 | 0302-9743 | 1 |
PageRank | References | Authors |
0.36 | 17 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Francesco Bongiovanni | 1 | 40 | 3.04 |
| Ludovic Henrio | 2 | 304 | 34.43 |