J. Bengtson and J. Parrow, Psi-calculi in Isabelle, Theorem Proving in Higher Order Logics, pp.99-114, 2009.
DOI : 10.1007/978-3-642-03359-9_9

S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith et al., Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations, Principles of Programming Languages (POPL'06), pp.55-66, 2006.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Conference on Automated Deduction (CADE-23), pp.116-130, 2011.
DOI : 10.1007/BFb0028402

T. Bourke, Mechanization of the Algebra for Wireless Networks (AWN) Archive of Formal Proofs, 2014.

T. Bourke, R. J. Van-glabbeek, and P. Höfner, A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol, Automated Technology for Verification and Analysis (ATVA'14), pp.47-63, 2014.
DOI : 10.1007/978-3-319-11936-6_5
URL : https://hal.archives-ouvertes.fr/hal-01092360

T. Bourke, R. J. Van-glabbeek, and P. Höfner, Showing Invariance Compositionally for a Process Algebra for Network Protocols, Interactive Theorem Proving (ITP'14), pp.144-159, 2014.
DOI : 10.1007/978-3-319-08970-6_10
URL : https://hal.archives-ouvertes.fr/hal-01092348

T. Bourke and P. Höfner, Loop freedom of the (untimed) aodv routing protocol. Archive of Formal Proofs, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01104033

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

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, Verifying Safety Properties with the TLA???+??? Proof System, Int. Joint Conference on Automated Reasoning (IJCAR'10), pp.142-148, 2010.
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821

A. Fehnker, R. J. Van-glabbeek, P. Höfner, A. K. Mciver, M. Portmann et al., A Process Algebra for Wireless Mesh Networks, European Symposium on Programming (ESOP '12), pp.295-315, 2012.
DOI : 10.1007/978-3-642-28869-2_15

A. Fehnker, R. J. Van-glabbeek, P. Höfner, A. K. Mciver, M. Portmann et al., A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV, p.7645, 2013.

A. Feliachi, M. C. Gaudel, and B. Wolff, Isabelle/Circus: A Process Specification and Verification Environment, Verified Software: Theories, Tools, and Experiments (VSTTE'12), pp.243-260, 2012.
DOI : 10.1007/978-3-642-14521-6_13

R. W. Floyd, Assigning meanings to programs, Proceedings of the Symposia in Applied Mathematics, pp.19-32, 1967.
DOI : 10.1007/978-94-011-1793-7_4

W. Fokkink, J. F. Groote, and M. Reniers, Process algebra needs proof methodology, In: EATCS Bulletin, vol.82, pp.109-125, 2004.

F. Ghassemi, W. Fokkink, and A. Movaghar, Restricted Broadcast Process Theory, 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pp.345-354, 2008.
DOI : 10.1109/SEFM.2008.25

J. C. Godskesen, A Calculus for Mobile Ad Hoc Networks, Coordination Models and Languages (COORDINATION '07), pp.132-150, 2007.
DOI : 10.1007/978-3-540-72794-1_8

T. Göthel and S. Glesner, An approach for machine-assisted verification of Timed CSP specifications, Innovations in Systems and Software Engineering, vol.40, issue.4, pp.181-193, 2010.
DOI : 10.1007/s11334-010-0126-z

B. Heyd, P. G. Crégut, J. Goos, J. Hartmanis, J. Leeuwen et al., A modular coding of UNITY in COQ, Theorem Proving in Higher Order Logics, pp.251-266, 1996.
DOI : 10.1007/BFb0105409

D. Hirschkoff, A full formalisation of ??-calculus theory in the calculus of constructions, Theorem Proving in Higher Order Logics, pp.153-169, 2007.
DOI : 10.1007/BFb0028392

F. Kammüller, M. Wenzel, and L. C. Paulson, Locales A Sectioning Concept for Isabelle, Theorem Proving in Higher Order Logics, pp.149-165, 1999.
DOI : 10.1007/3-540-48256-3_11

L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

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

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1995.
DOI : 10.1007/978-1-4612-4222-2

M. Merro, An Observational Theory for Mobile Ad Hoc Networks (full version), Information and Computation, vol.207, issue.2, pp.194-208, 2009.
DOI : 10.1016/j.ic.2007.11.010

N. Mezzetti and D. Sangiorgi, Towards a Calculus For Wireless Systems, Electronic Notes in Theoretical Computer Science, vol.158, pp.331-353, 2006.
DOI : 10.1016/j.entcs.2006.04.017
URL : http://doi.org/10.1016/j.entcs.2006.04.017

R. Milner, Operational and algebraic semantics of concurrent processes Handbook of Theoretical Computer Science, chap. 19 Alternatively see Communication and Concurrency, of which an earlier version appeared as A Calculus of Communicating Systems, pp.1201-1242, 1980.

O. Müller, A verification environment for I/O Automata based on formalized meta-theory, 1998.

S. Nanz and C. Hankin, A framework for security analysis of mobile wireless networks, Theoretical Computer Science, vol.367, issue.1-2, pp.203-227, 2006.
DOI : 10.1016/j.tcs.2006.08.036

L. C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, vol.6, issue.1-2, pp.85-128, 1998.
DOI : 10.3233/JCS-1998-61-205

C. E. Perkins, E. M. Belding-royer, and S. R. Das, Ad hoc on-demand distance vector (AODV) routing, Network Working Group, 2003.
DOI : 10.17487/rfc3561

G. Plotkin, A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60, pp.17-139, 1981.

A. Singh, C. R. Ramakrishnan, and S. A. Smolka, A process calculus for Mobile Ad Hoc Networks, Science of Computer Programming, vol.75, issue.6, pp.440-469, 2010.
DOI : 10.1016/j.scico.2009.07.008

W. P. De-roever, F. De-boer, U. Hannemann, J. Hooman, Y. Lakhnech et al., Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science CUP, vol.54, 2001.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

H. Tej and B. Wolff, A corrected failure-divergence model for CSP in Isabelle/HOL, Industrial Applications and Strengthened Foundations of Formal Methods (FME'97), pp.318-337, 1997.
DOI : 10.1007/3-540-63533-5_17

M. Wenzel, Isabelle/jEdit ??? A Prover IDE within the PIDE Framework, Intelligent Computer Mathematics, pp.468-471, 2012.
DOI : 10.1007/978-3-642-31374-5_38

M. Wenzel, Shared-Memory Multiprocessing for Interactive Theorem Proving, Interactive Theorem Proving (ITP'13), pp.418-434, 2013.
DOI : 10.1007/978-3-642-39634-2_30

M. Zhou, H. Yang, X. Zhang, and J. Wang, The proof of AODV loop freedom, 2009 International Conference on Wireless Communications & Signal Processing, 2009.
DOI : 10.1109/WCSP.2009.5371479