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

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

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

Y. Deng, S. Grumbach, and J. Monin, Coq script for Netlog protocols

Y. Deng, S. Grumbach, and J. Monin, Verifying Declarative Netlog Protocols with Coq: a First Experiment, Research Report, vol.7511, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00567811

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

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.

R. G. Gallager, P. A. Humblet, and P. M. Spira, A Distributed Algorithm for Minimum-Weight Spanning Trees, ACM Transactions on Programming Languages and Systems, vol.5, issue.1, pp.66-77, 1983.
DOI : 10.1145/357195.357200

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

W. H. Hesselink, The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract, Formal Aspects of Computing, vol.11, issue.1, pp.45-55, 1999.
DOI : 10.1007/s001650050035

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, 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, Distributed Algorithms, 1996.

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

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

Y. Moses and B. Shimony, A New Proof of the GHS Minimum Spanning Tree Algorithm, Lecture Notes in Computer Science, vol.4167, pp.120-135, 2006.
DOI : 10.1007/11864219_9

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

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

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. L. Welch, L. Lamport, and N. Lynch, A lattice-structured proof of a minimum spanning, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing , PODC '88, pp.28-43, 1988.
DOI : 10.1145/62546.62552

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