Towards Verifying Declarative Netlog Protocols with Coq

Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks.It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this paper, we show that moreover they provide a promising approach to the verification of distributed protocols. We choose the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq. Finally, we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed declarative protocols, as sketched on a concrete example, a breadth-first search tree construction in a distributed network