{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T15:45:57Z","timestamp":1756309557488,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319335995"},{"type":"electronic","value":"9783319336008"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_5","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T04:15:15Z","timestamp":1462853715000},"page":"86-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Rigorous Correctness Proof for Pastry"],"prefix":"10.1007","author":[{"given":"Noran","family":"Azmy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"5_CR1","unstructured":"LuPastry\n                      \n                        \n                      \n                      $$^+$$\n                      \n                        \n                          \n                            \n                            +\n                          \n                        \n                      \n                    : Specification and Proof Files. \n                      http:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/people\/noran-azmy\/"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2007.01.052","volume":"181","author":"R Bakhshi","year":"2007","unstructured":"Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: a case study. Electron. Notes Theor. Comput. Sci. 181, 35\u201347 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-31794-4_13","volume-title":"Global Computing","author":"J Borgstr\u00f6m","year":"2005","unstructured":"Borgstr\u00f6m, J., Nestmann, U., Onana, L., Gurov, D.: Verifying a structured peer-to-peer overlay network: the static case. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 250\u2013265. Springer, Heidelberg (2005)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-32759-9_14","volume-title":"FM 2012: Formal Methods","author":"D Cousineau","year":"2012","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA\n                      \n                        \n                      \n                      $$^{+}$$\n                      \n                        \n                          \n                            \n                            +\n                          \n                        \n                      \n                     proofs. In: M\u00e9ry, D., Giannakopoulou, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147\u2013154. Springer, Heidelberg (2012)"},{"key":"5_CR5","volume-title":"Specifying Systems: The TLA $$^+$$","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA\n                      \n                        \n                      \n                      $$^+$$\n                      \n                        \n                          \n                            \n                            +\n                          \n                        \n                      \n                     Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-319-25942-0_19","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"T Lu","year":"2015","unstructured":"Lu, T.: Formal verification of the pastry protocol using TLA\n                      \n                        \n                      \n                      $$^+$$\n                      \n                        \n                          \n                            \n                            +\n                          \n                        \n                      \n                    . In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 284\u2013299. Springer, Heidelberg (2015). doi:\n                      10.1007\/978-3-319-25942-0_19"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/3-540-45518-3_18","volume-title":"Middleware 2001","author":"A Rowstron","year":"2001","unstructured":"Rowstron, A., Druschel, P.: Pastry: scalable, decentralized object location, and routing for large-scale peer-to-peer systems. In: Guerraoui, R. (ed.) Middleware 2001. LNCS, vol. 2218, pp. 329\u2013350. Springer, Heidelberg (2001)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: a Scalable Peer-to-peer lookup service for internet applications. In: SIGCOMM 2001, pp. 149\u2013160. ACM (2001)","DOI":"10.1145\/964723.383071"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA\n                      \n                        \n                      \n                      $$^+$$\n                      \n                        \n                          \n                            \n                            +\n                          \n                        \n                      \n                     specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999)"},{"issue":"2","key":"5_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/2185376.2185383","volume":"42","author":"P Zave","year":"2012","unstructured":"Zave, P.: Using lightweight modeling to understand chord. ACM SIGCOMM Comput. Commun. Rev. 42(2), 49\u201357 (2012)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"5_CR11","unstructured":"Zave, P.: How to Make Chord Correct (Using a Stable Base). CoRR abs\/1502.06461 (2015)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33600-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T23:30:23Z","timestamp":1559431823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"11 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}