G. H. Fletcher, H. A. Sheth, and K. Börner, Unstructured peer-to-peer networks: Topological properties and search performance Agents and Peer-to-Peer Computing, LNCS, vol.3601, pp.14-27, 2004.

A. Rowstron and P. , Pastry: Scalable, Decentralized Object Location, and Routing for Large-Scale Peer-to-Peer Systems, Distributed Systems Platforms (Middleware'01), pp.329-350, 2001.
DOI : 10.1007/3-540-45518-3_18

URL : http://www.cs.uoi.gr/~pitoura/courses/p2p06/papers/pastry2.pdf

I. Stoica, R. Morris, D. Karger, M. F. Kaashoek, and H. Balakrishnan, Chord: A scalable peer-to-peer lookup service for Internet applications, Applications, Technologies, Architectures, and Protocols for Computer Communications, pp.149-160, 2001.

P. Maymounkov and D. , Mazì eres, Kademlia: A Peer-to-Peer Information System Based on the XOR Metric, in: Peer-to-Peer Systems, IPTPS'01), pp.53-65, 2002.

S. Ratnasamy, P. Francis, M. Handley, R. Karp, and S. Shenker, A Scalable Content-Addressable Network, Applications , Technologies, Architectures, and Protocols for Computer Communications, pp.161-172, 2001.
DOI : 10.1145/964723.383072

URL : http://www.cs.utexas.edu/users/browne/CS395Tf2002/Papers/Can-p161-ratnasamy.pdf

L. O. Alima, S. El-ansary, P. Brand, and S. Haridi, DKS (N , k , f ): A family of low communication, scalable and fault-tolerant infrastructures for p2p applications, Cluster Computing and the Grid, pp.344-350, 2003.

T. Lu, Formal Verification of the Pastry Protocol Using $$\mathrm{{TLA}}^{+}$$, Dependable Software Engineering: Theories, Tools, and Applications, pp.284-299, 2015.
DOI : 10.1007/978-3-319-25942-0_19

T. Lu, Formal Verification of the Pastry Protocol, 2013.
URL : https://hal.archives-ouvertes.fr/tel-01750356

A. Haeberlen, J. Hoye, A. Mislove, and P. , Consistent key mapping in structured overlays, 2005.

R. Bakhshi and D. Gurov, Verification of Peer-to-peer Algorithms: A Case Study, Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, pp.49-57, 2006.
DOI : 10.1016/j.entcs.2007.01.052

P. Zave, Using lightweight modeling to understand chord, ACM SIGCOMM Computer Communication Review, vol.42, issue.2, pp.49-57, 2012.
DOI : 10.1145/2185376.2185383

URL : http://www.sigcomm.org/sites/default/files/ccr/papers/2012/April/2185376-2185383.pdf

P. Zave, How to Make Chord Correct (Using a Stable Base, Computing Research Repository (CoRR), 2015.

A. Ghodsi, Distributed k-ary system: Algorithms for distributed hash tables, KTH Royal Institute of Technology, 2006.

J. Borgström, U. Nestmann, L. O. Alima, and D. Gurov, Verifying a Structured Peer-to-Peer Overlay Network: The Static Case, Global Computing, pp.250-265, 2004.
DOI : 10.1007/3-540-45518-3_18

T. Lu, S. Merz, and C. Weidenbach, Towards Verification of the Pastry Protocol Using TLA???+???, Formal Techniques for Distributed Systems, pp.244-258, 2011.
DOI : 10.1007/3-540-48153-2_6

URL : https://hal.archives-ouvertes.fr/hal-01583322

N. Azmy, S. Merz, C. Weidenbach, . Tla, and Z. Vdm, A Rigorous Correctness Proof for Pastry, Abstract State Machines, pp.86-101, 2016.
DOI : 10.1007/978-3-319-33600-8_5

URL : https://hal.archives-ouvertes.fr/hal-01322342

L. Lamport, Specifying Systems, 2002.

Y. Yu, P. Manolios, and L. Lamport, Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods (CHARME'99), pp.54-66, 1999.
DOI : 10.1007/3-540-48153-2_6

URL : http://www.cc.gatech.edu/fac/Pete.Manolios/pub/charme-proceedings.ps.gz

T. Bouton, D. Caminha-de-oliveira, D. Déharbe, and P. Fontaine, veriT: An open, trustable and efficient smt-solver Automated Deduction (CADE-22, LNCS, vol.5663, pp.151-156, 2009.
DOI : 10.1007/978-3-642-02959-2_12

URL : http://www.loria.fr/~fontaine/Bouton1.pdf

L. M. De-moura and N. Bjørner, Z3: an efficient SMT solver Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.4963, pp.337-340, 2008.

C. Weidenbach, D. Dimova, A. Fietzke, M. Suda, and P. Wischnewski, SPASS Version 3.5, Automated Deduction (CADE-22), pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Logic for Programming, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13

URL : https://hal.archives-ouvertes.fr/inria-00315920

L. C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994.
DOI : 10.1007/BFb0030541

M. Suda and C. Weidenbach, A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance, Automated Reasoning, pp.537-543, 2012.
DOI : 10.1007/978-3-642-31365-3_42