%O Report %F CASTERAN-2009-371705 %A Castéran, Pierre %A Filou, Vincent %A Mosbah, Mohamed %T {Formal Proofs of Local Computation Systems} %X {This paper describes the structure of a library for certifying distributed algorithms, contributed by Pierre Cast{é}ran and Vincent Filou. We formalize in the Coq proof assistant the behaviour of a subclass of local computation systems, namely the LC0 graph relabeling systems. We show how this formalization allows not only to build certified LC0 systems, but also study the limitations of their control structure.} %U http://hal.archives-ouvertes.fr/hal-00371705/PDF/description.pdf %8 March %D 2009