{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:42:25Z","timestamp":1779392545488,"version":"3.53.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030311568","type":"print"},{"value":"9783030311575","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-31157-5_10","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"147-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proving a Non-blocking Algorithm for Process Renaming with TLA $$^+$$ +"],"prefix":"10.1007","author":[{"given":"Aur\u00e9lie","family":"Hurault","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippe","family":"Qu\u00e9innec","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Afek, Y., Merritt, M.: Fast, wait-free (2k)-renaming. In: 18th Annual ACM Symposium on Principles of Distributed Computing, pp. 105\u2013112 (1999)","DOI":"10.1145\/301308.301338"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the $${\\rm TLA}^+$$ TLA + proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 142\u2013148. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_12"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Chuong, P., Ellen, F., Ramachandran, V.: A universal construction for wait-free transaction friendly data structures. In: 22nd ACM Symposium on Parallelism in Algorithms and Architectures, pp. 335\u2013344 (2010)","DOI":"10.1145\/1810479.1810538"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Castaneda, A., Hurault, A., Queinnec, P., Roy, M.: Modular machine-checked proofs of concurrent algorithms built from tasks. In: Submitted to DISC 2019 (2019)","DOI":"10.1007\/978-3-030-34992-9_6"},{"issue":"3","key":"10_CR5","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.cosrev.2011.04.001","volume":"5","author":"A Casta\u00f1eda","year":"2011","unstructured":"Casta\u00f1eda, A., Rajsbaum, S., Raynal, M.: The renaming problem in shared memory systems: an introduction. Comput. Sci. Rev. 5(3), 229\u2013251 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-39799-8_11","volume-title":"Computer Aided Verification","author":"C Dr\u0103goi","year":"2013","unstructured":"Dr\u0103goi, C., Gupta, A., Henzinger, T.A.: Automatic linearizability proofs of concurrent objects with cooperating updates. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 174\u2013190. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_11"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00446-004-0115-2","volume":"18","author":"H Gao","year":"2005","unstructured":"Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distrib. Comput. 18(1), 21\u201342 (2005)","journal-title":"Distrib. Comput."},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-27813-9_4","volume-title":"Computer Aided Verification","author":"H Gao","year":"2004","unstructured":"Gao, H., Hesselink, W.H.: A formal reduction for lock-free parallel algorithms. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 44\u201356. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_4"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Gu, R., et al.: Deep specifications and certified abstraction layers. In: 42nd ACM Symposium on Principles of Programming Languages, pp. 595\u2013608 (2015)","DOI":"10.1145\/2775051.2676975"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-16023-3_30","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"E Gafni","year":"2010","unstructured":"Gafni, E., Rajsbaum, S.: Recursion in distributed computing. In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds.) SSS 2010. LNCS, vol. 6366, pp. 362\u2013376. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16023-3_30"},{"issue":"1","key":"10_CR11","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"10_CR12","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1145\/161468.161469","volume":"15","author":"M Herlihy","year":"1993","unstructured":"Herlihy, M.: A methodology for implementing highly concurrent objects. ACM Trans. Program. Lang. Syst. 15(5), 745\u2013770 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR13","unstructured":"Hurault, A., Qu\u00e9innec, P.: $${\\rm TLA}^+$$ TLA + proof of Moir-Anderson renaming algorithm (2019). http:\/\/hurault.perso.enseeiht.fr\/RenamingProof"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR15","unstructured":"Bug JDK-6785442: ConcurrentLinkedQueue.remove() and poll() can both remove the same element (2008)"},{"key":"10_CR16","volume-title":"Distributed Computing: Principles, Algorithms, and Systems","author":"AD Kshemkalyani","year":"2011","unstructured":"Kshemkalyani, A.D., Singhal, M.: Distributed Computing: Principles, Algorithms, and Systems. Cambridge University Press, Cambridge (2011)"},{"issue":"2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1","author":"L Lamport","year":"1986","unstructured":"Lamport, L.: On interprocess communication. Distrib. Comput. 1(2), 77\u2013101 (1986)","journal-title":"Distrib. Comput."},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR19","volume-title":"Specifying Systems","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison Wesley, Boston (2002)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-03466-4_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"L Lamport","year":"2009","unstructured":"Lamport, L.: The PlusCal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36\u201360. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03466-4_2"},{"issue":"1","key":"10_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","volume":"11","author":"L Lamport","year":"2012","unstructured":"Lamport, L.: How to write a 21st century proof. J. Fixed Point Theory Appl. 11(1), 43\u201363 (2012)","journal-title":"J. Fixed Point Theory Appl."},{"issue":"1","key":"10_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(95)00009-H","volume":"25","author":"M Moir","year":"1995","unstructured":"Moir, M., Anderson, J.H.: Wait-free algorithms for fast, long-lived renaming. Sci. Comput. Program. 25(1), 1\u201339 (1995)","journal-title":"Sci. Comput. Program."},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Moir, M., Nussbaum, D., Shalev, O., Shavit, N.: Using elimination to implement scalable and lock-free FIFO queues. In: 17th ACM Symposium on Parallelism in Algorithms and Architectures, pp. 253\u2013262 (2005)","DOI":"10.1145\/1073970.1074013"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jpdc.1998.1446","volume":"51","author":"MM Michael","year":"1998","unstructured":"Michael, M.M., Scott, M.L.: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors. J. Parallel Distrib. Comput. 51(1), 1\u201326 (1998)","journal-title":"J. Parallel Distrib. Comput."},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: 29th ACM Symposium on Principles of Distributed Computing, pp. 85\u201394 (2010)","DOI":"10.1145\/1835698.1835722"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Rajsbaum, S., Raynal, M.: A theory-oriented introduction to wait-free synchronization based on the adaptive renaming problem. In: 25th IEEE International Conference on Advanced Information Networking and Applications, pp. 356\u2013363 (2011)","DOI":"10.1109\/AINA.2011.9"},{"issue":"6","key":"10_CR27","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s002240000072","volume":"30","author":"N Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Elimination trees and the construction of pools and stacks. Theory Comput. Syst. 30(6), 645\u2013670 (1997)","journal-title":"Theory Comput. Syst."},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Timnat, S., Petrank, E.: A practical wait-free simulation for lock-free data structures. In: ACM Symposium on Principles and Practice of Parallel Programming, PPoPP 2014, pp. 357\u2013368 (2014)","DOI":"10.1145\/2692916.2555261"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-10181-1_22","volume-title":"Integrated Formal Methods","author":"B Tofan","year":"2014","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: A compositional proof method for linearizability applied to a wait-free multiset. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 357\u2013372. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_22"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31157-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T18:55:25Z","timestamp":1575744925000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31157-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030311568","9783030311575"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31157-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tap.sosy-lab.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}