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
What happened on august 16, Blog, 2007. ,
Basic paramodulation and superposition, 1992. ,
DOI : 10.1007/3-540-55602-8_185
Principles of model checking, volume 26202649, 2008. ,
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
Mathematical logic for computer science, 2012. ,
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
Symbolic model checking without BDDs, 1999. ,
Bounded model checking Advances in computers, pp.117-148, 2003. ,
High availability, scalable storage, dynamic peer networks: Pick two, 9th Workshop on Hot Topics in Operating Systems (HotOS), p.21, 2003. ,
Zeit Online, 2012. ,
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. ,
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
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
Virtual ring routing, ACM SIGCOMM Computer Communication Review, vol.36, issue.4, pp.351-362, 2006. ,
DOI : 10.1145/1151659.1159954
Proximity neighbor selection in tree-based structured peer-to-peer overlays, 2003. ,
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
Why software fails, 2005. ,
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
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
The birth of model checking, 25 Years of Model Checking, pp.1-26, 2008. ,
Formal methods: State of the art and future directions, ACM Computing Surveys (CSUR), vol.28, issue.4, pp.626-643, 1996. ,
Exploiting symmetry in temporal logic model checking, Computer Aided Verification, pp.450-462, 1993. ,
Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.16, issue.5, pp.1512-1542, 1994. ,
Incentives build robustness in bittorrent In Workshop on Economics of Peer-to-Peer systems, pp.68-72, 2003. ,
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
Z3: An efficient smt solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008. ,
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. ,
Software horror stories, 2013. ,
The yices smt solver, 2006. ,
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. ,
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
First-order logic and automated theorem proving, 1996. ,
Pastry: A substrate for peer-to-peer applications, 2009. ,
Distributed k-ary system: Algorithms for distributed hash tables, 2006. ,
What does skype's architecture do?, 2012. ,
Using partial orders to improve automatic verification methods, Computer-Aided Verification, pp.176-185, 1991. ,
DOI : 10.1007/bfb0023731
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 ,
25 years of model checking: history, achievements, perspectives, 2008. ,
DOI : 10.1007/978-3-540-69850-0
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
Consistent key mapping in structured overlays, 2005. ,
Skype blames outage on " supernode " problem, 2010. URL http://www.itbusiness.ca/news/ skype-blames-outage-on-supernode-problem, 14322. ,
Toward network data independence, ACM SIGMOD Record, vol.32, issue.3, pp.34-40, 2003. ,
Industrial-strength formal methods in practice, 1999. ,
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. ,
TLA tools, 2012a. URL http ,
"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
Specifying Systems, The TLA + Language and Tools for Hardware and Software Engineers, 2002. ,
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
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. ,
Active and Concurrent Topology Maintenance, Distributed Computing, pp.320-334, 2004. ,
DOI : 10.1007/978-3-540-30186-8_23
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
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
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
Multichord: A resilient namespace management protocol. 2004. marketerterryb. Skype outage today, 2010. ,
Symbolic model checking, 1993. ,
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
About skype: What are p2p communications?, 2013. URL https ,
Illustrative risks to the public in the use of computer systems and related technology. Webpage, 04 2013 ,
Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006. ,
DOI : 10.1145/1217856.1217859
Isabelle/HOL: a proof assistant for higher-order logic, volume 2283, 2002. ,
DOI : 10.1007/3-540-45949-9
Peer-to-peer: harnessing the benefits of a disruptive technology, 2001. ,
The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.5, 1989. ,
Combining partial order reductions with on-the-fly model-checking, Computer aided verification, pp.377-390, 1994. ,
A scalable content-addressable network, 2001. ,
Handling churn in a DHT, 2003. ,
Vampire 1.1 (system description), Proceedings of the First International Joint Conference on Automated Reasoning, IJCAR '01, pp.376-380, 2001. ,
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
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
Peer-to-peer systems, Communications of the ACM, vol.53, issue.10, pp.72-82, 2010. ,
DOI : 10.1145/1831407.1831427
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
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. ,
E-a brainiac theorem prover, pp.111-126, 2002. ,
An introduction to formal hardware verification, 1992. ,
Chord, ACM SIGCOMM Computer Communication Review, vol.31, issue.4, pp.149-160, 2001. ,
DOI : 10.1145/964723.383071
A stubborn attack on state explosion, Computer-Aided Verification, pp.156-165, 1991. ,
The TLA + codes for the pastry model, 2013. ,
SPASS & FLOTTER version 0.42, CADE, pp.141-145, 1996. ,
DOI : 10.1007/3-540-61511-3_75
The Isabelle Framework, Theorem Proving in Higher Order Logics, pp.33-38, 2008. ,
DOI : 10.1007/978-3-540-74591-4_26
Understanding today's skype outage: Explaining supern- odes, 2010. ,
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
Using lightweight modeling to understand chord, ACM SIGCOMM Computer Communication Review, vol.42, issue.2, pp.49-57, 2012. ,
DOI : 10.1145/2185376.2185383
Tapestry: A resilient global-scale overlay for service deployment. Selected Areas in Communications, IEEE Journal on, vol.22, issue.1, pp.41-53, 2004. ,