Unstructured peer-to-peer networks: Topological properties and search performance Agents and Peer-to-Peer Computing, LNCS, vol.3601, pp.14-27, 2004. ,
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
Chord: A scalable peer-to-peer lookup service for Internet applications, Applications, Technologies, Architectures, and Protocols for Computer Communications, pp.149-160, 2001. ,
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. ,
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
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. ,
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
Formal Verification of the Pastry Protocol, 2013. ,
URL : https://hal.archives-ouvertes.fr/tel-01750356
Consistent key mapping in structured overlays, 2005. ,
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
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
How to Make Chord Correct (Using a Stable Base, Computing Research Repository (CoRR), 2015. ,
Distributed k-ary system: Algorithms for distributed hash tables, KTH Royal Institute of Technology, 2006. ,
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
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
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
Specifying Systems, 2002. ,
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
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
Z3: an efficient SMT solver Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.4963, pp.337-340, 2008. ,
SPASS Version 3.5, Automated Deduction (CADE-22), pp.140-145, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
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
Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994. ,
DOI : 10.1007/BFb0030541
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