S. Androutsellis-theotokis and D. Spinellis, A survey of peer-to-peer content distribution technologies, ACM Computing Surveys, vol.36, issue.4, pp.335-371, 2004.
DOI : 10.1145/1041680.1041681

V. Arak, What happened on august 16, Blog, 2007.

L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic paramodulation and superposition, 1992.
DOI : 10.1007/3-540-55602-8_185

C. Baier and J. Katoen, Principles of model checking, volume 26202649, 2008.

R. Bakhshi and D. Gurov, Verification of Peer-to-peer Algorithms: A Case Study, Electronic Notes in Theoretical Computer Science, vol.181, pp.35-47, 2007.
DOI : 10.1016/j.entcs.2007.01.052

M. Ben-ari, Mathematical logic for computer science, 2012.

Y. Bertot and P. Castéran, Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions, 2004.
DOI : 10.1007/978-3-662-07964-5

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

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic model checking without BDDs, 1999.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded model checking Advances in computers, pp.117-148, 2003.

C. Blake and R. Rodrigues, High availability, scalable storage, dynamic peer networks: Pick two, 9th Workshop on Hot Topics in Operating Systems (HotOS), p.21, 2003.

N. Boeing, . Das, and . Internet, Zeit Online, 2012.

F. A. Bongiovanni, Design, Formalization and Implementation of Overlay Networks ; Application to RDF Data Storage Ecole doctorale STIC science et technologies de l'information et de la communication, 2012.

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

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

J. Borgström, U. Nestmann, L. Onana-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

M. Caesar, M. Castro, E. B. Nightingale, G. O. Shea, and A. Rowstron, Virtual ring routing, ACM SIGCOMM Computer Communication Review, vol.36, issue.4, pp.351-362, 2006.
DOI : 10.1145/1151659.1159954

M. Castro, P. Druschel, Y. C. Hu, and A. Rowstron, Proximity neighbor selection in tree-based structured peer-to-peer overlays, 2003.

M. Castro, M. Costa, and A. I. Rowstron, Performance and dependability of structured peer-to-peer overlays, International Conference on Dependable Systems and Networks, 2004, pp.9-18, 2004.
DOI : 10.1109/DSN.2004.1311872

R. N. Charette, Why software fails, 2005.

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, Verifying Safety Properties with the TLA???+??? Proof System, Lecture Notes in Computer Science, vol.6173, pp.142-148
DOI : 10.1007/978-3-642-14203-1_12

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

Y. Chawathe, S. Ratnasamy, L. Breslau, N. Lanham, and S. Shenker, Making gnutella-like P2P systems scalable, Proceedings of the 2003 conference on Applications, technologies, architectures, and protocols for computer communications , SIGCOMM '03, pp.407-418, 2003.
DOI : 10.1145/863955.864000

URL : http://berkeley.intel-research.net/sylvia/1103-chawathe.pdf

M. Edmund and . Clarke, The birth of model checking, 25 Years of Model Checking, pp.1-26, 2008.

M. Edmund, J. M. Clarke, and . Wing, Formal methods: State of the art and future directions, ACM Computing Surveys (CSUR), vol.28, issue.4, pp.626-643, 1996.

M. Edmund, T. Clarke, S. Filkorn, and . Jha, Exploiting symmetry in temporal logic model checking, Computer Aided Verification, pp.450-462, 1993.

M. Edmund, O. Clarke, . Grumberg, E. David, and . Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.16, issue.5, pp.1512-1542, 1994.

B. Cohen, Incentives build robustness in bittorrent In Workshop on Economics of Peer-to-Peer systems, pp.68-72, 2003.

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA???+??? Proofs, FM 2012: Formal Methods, pp.147-154, 2012.
DOI : 10.1007/978-3-642-32759-9_14

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

L. De, M. , and N. Bjørner, Z3: An efficient smt solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.

G. Decandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman et al., Dynamo: amazon's highly available key-value store, ACM Symposium on Operating Systems Principles: Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pp.205-220, 2007.

N. Dershowitz, Software horror stories, 2013.

B. Dutertre and L. D. Moura, The yices smt solver, 2006.

E. Allen, E. Joseph, and Y. Halpern, Sometimes " and " not never " revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), vol.33, issue.1, pp.151-178, 1986.

G. Fersi, W. Louati, and M. Jemaa, Distributed Hash table-based routing and data management in wireless sensor networks: a survey, Wireless Networks, vol.12, issue.1951, pp.219-236, 2013.
DOI : 10.1109/WONS.2009.4801850

M. Fitting, First-order logic and automated theorem proving, 1996.

. Freepastry, Pastry: A substrate for peer-to-peer applications, 2009.

A. Ghodsi, Distributed k-ary system: Algorithms for distributed hash tables, 2006.

M. Gillett, What does skype's architecture do?, 2012.

P. Godefroid, Using partial orders to improve automatic verification methods, Computer-Aided Verification, pp.176-185, 1991.
DOI : 10.1007/bfb0023731

D. Goodin, Skype replaces P2P supernodes with linux boxes hosted by microsoft (updated), 2012. URL http://arstechnica.com/business/2012/05/ skype-replaces-p2p-supernodes-with-linux-boxes-hosted-by-microsoft

O. Grumberg and H. Veith, 25 years of model checking: history, achievements, perspectives, 2008.
DOI : 10.1007/978-3-540-69850-0

K. Gummadi, R. Gummadi, S. Gribble, S. Ratnasamy, S. Shenker et al., The impact of DHT routing geometry on resilience and proximity, Proceedings of the 2003 conference on Applications, technologies, architectures, and protocols for computer communications , SIGCOMM '03, pp.381-394, 2003.
DOI : 10.1145/863955.863998

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

E. Heichler and J. Newman, Skype blames outage on " supernode " problem, 2010. URL http://www.itbusiness.ca/news/ skype-blames-outage-on-supernode-problem, 14322.

M. Joseph and . Hellerstein, Toward network data independence, ACM SIGMOD Record, vol.32, issue.3, pp.34-40, 2003.

M. Gerard, H. , and J. P. Bowen, Industrial-strength formal methods in practice, 1999.

M. Karsten, S. Keshav, S. Prasad, and M. Beg, An axiomatic basis for communication, Proceedings of the ACM SIGCOMM 2007 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, pp.217-228, 2007.

L. Lamport, TLA tools, 2012a. URL http

L. Lamport, "Sometime" is sometimes "not never", Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.174-185, 1980.
DOI : 10.1145/567446.567463

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

L. Lamport, How to write a 21st century proof, Journal of Fixed Point Theory and Applications, vol.16, issue.5, pp.43-63, 2012.
DOI : 10.1145/186025.186058

D. Lehmann and M. O. Rabin, On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '81, pp.133-138, 1981.

X. Li, J. Misra, and G. Plaxton, Active and Concurrent Topology Maintenance, Distributed Computing, pp.320-334, 2004.
DOI : 10.1007/978-3-540-30186-8_23

D. Loguinov, A. Kumar, V. Rai, and S. Ganesh, Graph-theoretic analysis of structured peer-to-peer systems, Proceedings of the 2003 conference on Applications, technologies, architectures, and protocols for computer communications , SIGCOMM '03, pp.395-406, 2003.
DOI : 10.1145/863955.863999

T. Lu, S. Merz, and C. Weidenbach, Model checking the Pastry routing protocol, 10th Intl. Workshop Automatic Verification of Critical Systems (AVOCS), pp.19-21, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00540811

T. Lu, S. Merz, and C. Weidenbach, Towards verification of the pastry protocol using TLA + . Research Report MPI-I-2011-RG1-002, p.66123, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01583322

N. Lynch and I. Stoica, Multichord: A resilient namespace management protocol. 2004. marketerterryb. Skype outage today, 2010.

L. Kenneth and . Mcmillan, Symbolic model checking, 1993.

S. Merz, The Specification Language TLA+, Logics of Specification Languages, Monographs in Theoretical Computer Science, pp.401-451, 2008.
DOI : 10.1007/978-3-540-74107-7_8

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

. Microsoft, About skype: What are p2p communications?, 2013. URL https

G. Peter and . Neumann, Illustrative risks to the public in the use of computer systems and related technology. Webpage, 04 2013

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

T. Nipkow, C. Lawrence, M. Paulson, and . Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, volume 2283, 2002.
DOI : 10.1007/3-540-45949-9

A. Oram, Peer-to-peer: harnessing the benefits of a disruptive technology, 2001.

C. Lawrence and . Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.5, 1989.

D. Peled, Combining partial order reductions with on-the-fly model-checking, Computer aided verification, pp.377-390, 1994.

S. Ratnasamy, P. Francis, M. Handley, R. Karp, and S. Shenker, A scalable content-addressable network, 2001.

S. Christopher-rhea, D. Geels, T. Roscoe, and J. Kubiatowicz, Handling churn in a DHT, 2003.

A. Riazanov and A. Voronkov, Vampire 1.1 (system description), Proceedings of the First International Joint Conference on Automated Reasoning, IJCAR '01, pp.376-380, 2001.

J. Risson and T. Moors, Survey of research towards robust peer-to-peer networks: Search methods, Computer Networks, vol.50, issue.17, pp.3485-3521, 2006.
DOI : 10.1016/j.comnet.2006.02.001

J. Risson, K. Robinson, and T. Moors, Fault Tolerant Active Rings for Structured Peer-to-Peer Overlays, The IEEE Conference on Local Computer Networks 30th Anniversary (LCN'05)l, pp.18-25, 2005.
DOI : 10.1109/LCN.2005.69

R. Rodrigues and P. Druschel, Peer-to-peer systems, Communications of the ACM, vol.53, issue.10, pp.72-82, 2010.
DOI : 10.1145/1831407.1831427

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

R. Schollmeier, A definition of peer-to-peer networking for the classification of peerto-peer architectures and applications, Peer-to-Peer Computing Proceedings. First International Conference on, pp.101-102, 2001.

S. Schulz, E-a brainiac theorem prover, pp.111-126, 2002.

C. Seger, An introduction to formal hardware verification, 1992.

I. Stoica, R. Morris, D. Karger, F. Kaashoek, and H. Balakrishnan, Chord, ACM SIGCOMM Computer Communication Review, vol.31, issue.4, pp.149-160, 2001.
DOI : 10.1145/964723.383071

A. Valmari, A stubborn attack on state explosion, Computer-Aided Verification, pp.156-165, 1991.

. Veridis, The TLA + codes for the pastry model, 2013.

C. Weidenbach, B. Gaede, and G. Rock, SPASS & FLOTTER version 0.42, CADE, pp.141-145, 1996.
DOI : 10.1007/3-540-61511-3_75

M. Wenzel, C. Lawrence, T. Paulson, and . Nipkow, The Isabelle Framework, Theorem Proving in Higher Order Logics, pp.33-38, 2008.
DOI : 10.1007/978-3-540-74591-4_26

D. York, Understanding today's skype outage: Explaining supern- odes, 2010.

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

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

Y. Ben, L. Zhao, J. Huang, . Stribling, C. Sean et al., Tapestry: A resilient global-scale overlay for service deployment. Selected Areas in Communications, IEEE Journal on, vol.22, issue.1, pp.41-53, 2004.