Mechanical Support for Efficient Dissemination on the CAN Overlay Network
Francesco Bongiovanni, Ludovic Henrio · HAL (Le Centre pour la Communication Scientifique Directe) · 2011
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.