M. Abadi and B. T. Loo, Towards a declarative language and system for secure networking, Proc. NETB'07, pp.1-6, 2007.

G. Alonso, E. Kranakis, C. Sawchuk, R. Wattenhofer, and P. Widmayer, Probabilistic Protocols for Node Discovery in Ad Hoc Multi-channel Broadcast Networks, Proc. ADHOC-NOW'03, 2003.
DOI : 10.1007/978-3-540-39611-6_10

M. Bauderon, Y. Métivier, M. Mosbah, and A. Sellami, Graph Relabelling Systems A Tool for Encoding, Proving, Studying and Visualizing Distributed Algorithms, Electronic Notes in Theoretical Computer Science, vol.51, issue.1, p.51, 2001.
DOI : 10.1016/S1571-0661(04)00194-X
URL : https://hal.archives-ouvertes.fr/hal-00307013

Y. Bejerano, Y. Breitbart, M. N. Garofalakis, and R. Rastogi, Physical topology discovery for large multi-subnet networks, Proc. INFOCOM'03, 2003.
DOI : 10.1109/infcom.2003.1208686
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.6414

Y. Bejerano, Y. Breitbart, A. Orda, R. Rastogi, and A. Sprintson, Algorithms for computing qos paths with restoration, IEEE/ACM Trans. Netw, vol.13, issue.3, 2005.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

K. M. Chandy, Parallel Program Design, 1988.
DOI : 10.1007/978-1-4613-9668-0_6

. Coq, The coq proof assistant reference manual
URL : https://hal.archives-ouvertes.fr/inria-00069919

. Coq, The Coq user contributions

A. J. Demers, J. Gehrke, R. Rajaraman, A. Trigoni, and Y. Yao, The Cougar Project, ACM SIGMOD Record, vol.32, issue.4, pp.53-59, 2003.
DOI : 10.1145/959060.959070

Y. Deng and J. Monin, Verifying Self-stabilizing Population Protocols with Coq, 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.201-208, 2009.
DOI : 10.1109/TASE.2009.9

E. Giménez, A Calculus of Infinite Constructions and its application to the verification of communicating systems, 1996.

S. Grumbach and F. Wang, Netlog, a Rule-Based Language for Distributed Programming, Proc. PADL'10, pp.88-103, 2010.
DOI : 10.1007/978-3-642-11503-5_9

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Proc. POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

C. Liu, Y. Mao, M. Oprea, P. Basu, and B. T. Loo, A declarative perspective on adaptive manet routing, Proceedings of the ACM workshop on Programmable routers for extensible services of tomorrow, PRESTO '08, pp.63-68, 2008.
DOI : 10.1145/1397718.1397733

B. T. Loo, T. Condie, M. N. Garofalakis, D. E. Gay, J. M. Hellerstein et al., Declarative networking, Proceedings of the 2006 ACM SIGMOD international conference on Management of data , SIGMOD '06, 2006.
DOI : 10.1145/1142473.1142485

B. T. Loo, T. Condie, J. M. Hellerstein, P. Maniatis, T. Roscoe et al., Implementing declarative overlays, Proc. SOSP'05, 2005.

B. T. Loo, J. M. Hellerstein, I. Stoica, and R. Ramakrishnan, Declarative routing: extensible routing with declarative queries, Proc. ACM SIGCOMM '05, 2005.

N. A. Lynch and M. R. Tuttle, An introduction to input/output automata, CWI Quarterly, vol.2, pp.219-246, 1989.

S. Madden, M. J. Franklin, J. M. Hellerstein, and W. Hong, TinyDB: an acquisitional query processing system for sensor networks, ACM Transactions on Database Systems, vol.30, issue.1, 2005.
DOI : 10.1145/1061318.1061322

G. Mainland, G. Morrisett, and M. Welsh, Flask: staged functional programming for sensor networks, Proc. ICFP'08, 2008.

Y. Métivier and E. Sopena, Graph relabelling systems: A general overview, Computers and Artificial Intelligence, vol.16, issue.2, 1997.

J. Monin, Proving a real time algorithm for ATM in Coq, Types for Proofs and Programs, pp.277-293, 1998.
DOI : 10.1007/BFb0097797

C. Paulin-mohring, Circuits as streams in Coq: Verification of a sequential multiplier, Proc. TYPES'96, pp.216-230, 1996.
DOI : 10.1007/3-540-61780-9_72

K. J. Turner, Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL, 1993.

A. Wang, P. Basu, B. T. Loo, and O. Sokolsky, Declarative Network Verification, PADL '09: Proceedings of the 11th International Symposium on Practical Aspects of Declarative Languages, pp.61-75, 2009.
DOI : 10.1016/0743-1066(94)00039-9