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. © 2013 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Bongiovanni, F., & Henrio, L. (2013). A mechanized model for CAN protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7793 LNCS, pp. 266–281). https://doi.org/10.1007/978-3-642-37057-1_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
