M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. POPL'01, pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

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. INFO- COM'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

B. Blanchet, Automatic verification of correspondences for security protocols*, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.
DOI : 10.3233/JCS-2009-0339

P. Castéran and V. Filou, Tâches, types et tactiques pour les systèmes de calculs locaux, Journées Francophones des Langages Applicatifs. Inria, 2010.

P. Castéran and V. Filou, Tasks, Types and Tactics for Local Computation Systems, Studia Informatica Universalis, 2011.

P. Castéran, V. Filou, and M. Mosbah, Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant, Symbolic Computation in Software Science (SCSS'09), 2009.

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

B. Chetali, Formal verification of concurrent programs using the Larch prover, IEEE Transactions on Software Engineering, vol.24, issue.1, pp.46-62, 1998.
DOI : 10.1109/32.663997
URL : https://hal.archives-ouvertes.fr/inria-00074199

R. Cleaveland, J. Parrow, and B. Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.36-72, 1993.
DOI : 10.1145/151646.151648

. Coq, The Coq Proof Assistant Reference Manual
URL : https://hal.archives-ouvertes.fr/inria-00069919

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, S. Grumbach, and J. Monin, Coq script for Netlog protocols

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.1221

J. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez et al., A toolbox for the verification of LOTOS programs, Proc. ICSE '92, pp.246-259, 1992.

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

R. Gotzhein and J. Bredereke, Formal Description Techniques IX: Theory, application and tools, IFIP Conference Proceedings. Chapman & Hall, 1996.
DOI : 10.1007/978-0-387-35079-0

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

B. Heyd and P. Crégut, A modular coding of UNITY in COQ, Proc. TPHOLs'96, pp.251-266, 1996.
DOI : 10.1007/BFb0105409

C. A. Hoare, Communicating Sequential Processes, 1985.

C. Jard, J. F. Monin, and R. Groz, Development of Veda, a prototyping tool for distributed algorithms, IEEE Transactions on Software Engineering, vol.14, issue.3, pp.339-352, 1988.
DOI : 10.1109/32.4654
URL : https://hal.archives-ouvertes.fr/inria-00071322

C. Kirkwood and M. Thomas, Experiences with specification and verification in LOTOS: a report on two case studies, Proceedings of 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques, p.159, 1995.
DOI : 10.1109/WIFT.1995.515487

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

T. Långbacka, A HOL formalisation of the Temporal Logic of Actions, Proc. TPHOL'94, pp.332-345, 1994.
DOI : 10.1007/3-540-58450-1_52

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.
DOI : 10.1145/1095809.1095818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.192.3367

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

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
DOI : 10.1007/3-540-61780-9_72

L. C. Paulson, Mechanizing UNITY in Isabelle, ACM Transactions on Computational Logic, vol.1, issue.1, pp.3-32, 2000.
DOI : 10.1145/343369.343370

F. Regensburger and A. Barnard, Formal verification of SDL systems at the siemens mobile phone department, Proc. TACAS '98, pp.439-455, 1998.
DOI : 10.1007/BFb0054188

A. W. Roscoe, Model-checking CSP, chapter 21, 1994.

S. M. Shahrier and R. M. Jenevein, SDL Specification and Verification of a Distributed Access Generic opticalNetwork Interface for SMDS Networks, 1997.

M. Törö, J. Zhu, and V. C. Leung, SDL specification and verification of universal personal computing: with Object GEODE, Proc. FORTE XI / PSTV XVIII '98, pp.267-282, 1998.

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, Proc. PADL '09, pp.61-75, 2009.
DOI : 10.1016/0743-1066(94)00039-9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.6502

J. Wu and S. T. Chanson, Translation from LOTOS and Estelle Specifications to Extended Transition System and its Verification, Proc. FORTE '89, pp.533-549, 1990.

W. Zhang, Applying SDL Specifications and Tools to the Verification of Procedures, Proc. SDL '01, pp.421-438, 2001.
DOI : 10.1007/3-540-48213-X_26