HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Mechanical Support for Efficient Dissemination on the CAN Overlay Network

Francesco Bongiovanni 1 Ludovic Henrio 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The various algorithms underlying P2P systems are notoriously difficult to design and analyze. Coming up with new proven algorithms for such large scale systems is a challenging task. We report on the initial steps of an ongoing work that aims to devise an efficient correct-by-construction broadcast algorithm for the CAN structured overlay network. To rigorously reason about such an algorithm and prove correctness we rely on an interactive theorem prover : Isabelle/HOL. This paper presents a generic reasoning framework which should ease the promotion of formal correctness proofs of existing multicast algorithms and also facilitate the design of new ones.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Francesco Bongiovanni Connect in order to contact the contributor
Submitted on : Wednesday, April 13, 2011 - 10:41:53 AM
Last modification on : Friday, February 4, 2022 - 3:19:54 AM
Long-term archiving on: : Thursday, November 8, 2012 - 4:15:18 PM


Files produced by the author(s)


  • HAL Id : inria-00585057, version 1



Francesco Bongiovanni, Ludovic Henrio. Mechanical Support for Efficient Dissemination on the CAN Overlay Network. [Research Report] RR-7599, INRIA. 2011. ⟨inria-00585057⟩



Record views


Files downloads