%0 Conference Proceedings %F MERY-2010-547302 %A Méry, Dominique %A Mosbah, Mohammed %A Tounsi, Mohammed %T Proving Distributed Algorithms by Combining Refinement and Local Computations %B AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems %E Jens Bendisposto, Michael Leuschel, Markus Roggenbach %C Dusseldorf, Allemagne %X Abstract: Our approach is directly related to the design of correct-by-construction programs. The main idea relies upon the development of distributed algorithms fol- lowing a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use the refinement for controlling the correctness of the resulting algorithm. It relies on a more fundamental question related to the notion of problem to solve. The methodology can be based on incremental proof-based developments. However, the link between the problem and the first model remains to be expressed and the refine- ment is a real help to justify in a very progressive way the choices of design. We propose in this work a framework combining local computations and refinement to prove the correctness of a large class of distributed algorithms %U http://hal.inria.fr/inria-00547302 %8 September %D 2010