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 <>
Submitted on : Wednesday, April 13, 2011 - 10:41:53 AM
Last modification on : Monday, October 12, 2020 - 10:30:26 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