{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:30:42Z","timestamp":1757626242673,"version":"3.44.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031954962"},{"type":"electronic","value":"9783031954979"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-95497-9_9","type":"book-chapter","created":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T13:15:40Z","timestamp":1749906940000},"page":"154-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Revisited Convergence of a Self-stabilizing BFS Spanning Tree Algorithm"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8344-1853","authenticated-orcid":false,"given":"Karine","family":"Altisen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4412-5684","authenticated-orcid":false,"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. Log. Methods Comput. Sci. 13(4) (2017)","DOI":"10.23638\/LMCS-13(4:14)2017"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: Squeezing streams and composition of self-stabilizing algorithms. In: P\u00e9rez, J.A., Yoshida, N. (eds.) FORTE 2019. LNCS, vol. 11535, pp. 21\u201338. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-21759-4_2","DOI":"10.1007\/978-3-030-21759-4_2"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: Certification of an exact worst-case selfstabilization time. In: ICDCN, pp. 46\u201355. ACM (2021)","DOI":"10.1145\/3427796.3427832"},{"key":"9_CR4","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: Certified round complexity of self-stabilizing algorithms. In: DISC. LIPIcs, vol.\u00a0281, pp. 2:1\u20132:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Altisen, K., Devismes, S., Dubois, S., Petit, F.: Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2019)","DOI":"10.1007\/978-3-031-02013-1"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Auger, C., Bouzid, Z., Courtieu, P., Tixeuil, S., Urbain, X.: Certified impossibility results for byzantine-tolerant mobile robots. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) SSS 2013. LNCS, vol. 8255, pp. 178\u2013190. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03089-0_13","DOI":"10.1007\/978-3-319-03089-0_13"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Softw. Tools Technol. Transf. 23(5), 797\u2013821 (2021)","DOI":"10.1007\/s10009-020-00603-x"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2015)","DOI":"10.1007\/978-3-031-02011-7"},{"issue":"1","key":"9_CR10","first-page":"39","volume":"9","author":"P Cast\u00e9ran","year":"2011","unstructured":"Cast\u00e9ran, P., Filou, V.: Tasks, types and tactics for local computation systems. Stud. Inform. Univ. 9(1), 39\u201386 (2011)","journal-title":"Stud. Inform. Univ."},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 120\u2013134. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24550-3_11","DOI":"10.1007\/978-3-642-24550-3_11"},{"issue":"2\u20133","key":"9_CR12","first-page":"273","volume":"3","author":"B Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. Int. J. Softw. Inform. 3(2\u20133), 273\u2013303 (2009)","journal-title":"Int. J. Softw. Inform."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Courtieu, P.: Proving self-stabilization with a proof assistant. In: IPDPS. IEEE Computer Society (2002)","DOI":"10.1109\/IPDPS.2002.1016619"},{"issue":"3","key":"9_CR14","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/j.ipl.2014.11.001","volume":"115","author":"P Courtieu","year":"2015","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115(3), 447\u2013452 (2015)","journal-title":"Inf. Process. Lett."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: FM. Lecture Notes in Computer Science, vol.\u00a07436, pp. 147\u2013154. Springer (2012)","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-41527-2_19","volume-title":"Distributed Computing","author":"C Delporte-Gallet","year":"2013","unstructured":"Delporte-Gallet, C., Fauconnier, H., Gafni, E., Lamport, L.: Adaptive register allocation with a linear number of registers. In: Afek, Y. (ed.) DISC 2013. LNCS, vol. 8205, pp. 269\u2013283. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41527-2_19"},{"issue":"11","key":"9_CR17","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF02278851","volume":"7","author":"S Dolev","year":"1993","unstructured":"Dolev, S., Israeli, A., Moran, S.: Self-stabilization of dynamic systems assuming only Read\/Write atomicity. Distrib. Comput. 7(1), 3\u201316 (1993)","journal-title":"Distrib. Comput."},{"key":"9_CR19","unstructured":"Ebnenasir, A.: Synthesizing self-stabilizing parameterized protocols with unbounded variables. In: FMCAD, pp. 245\u2013254. IEEE (2022)"},{"issue":"9","key":"9_CR20","doi-asserted-by":"publisher","first-page":"1622","DOI":"10.1016\/j.scico.2013.03.003","volume":"78","author":"WH Hesselink","year":"2013","unstructured":"Hesselink, W.H.: Mechanical verification of Lamport\u2019s Bakery algorithm. Sci. Comput. Program. 78(9), 1622\u20131638 (2013)","journal-title":"Sci. Comput. Program."},{"key":"9_CR21","unstructured":"Jaskelioff, M., Merz, S.: Proving the correctness of disk paxos. Archive of Formal Proofs 2005 (2005)"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: formal verification of distributed algorithms. In: Baeten, J., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_15","DOI":"10.1007\/978-3-642-33475-7_15"},{"key":"9_CR23","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)"},{"issue":"1","key":"9_CR24","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."},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.scico.2017.05.009","volume":"148","author":"V Rahli","year":"2017","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: EventML: specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148, 26\u201348 (2017)","journal-title":"Sci. Comput. Program."},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Rahli, V., Vukotic, I., V\u00f6lp, M., Esteves-Verissimo, P.: Velisarios: byzantine fault-tolerant protocols powered by Coq. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 619\u2013650. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_22","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"9_CR27","unstructured":"Rocq Team: The Rocq Prover (2025). https:\/\/rocq-prover.org\/"},{"issue":"1","key":"9_CR28","first-page":"81","volume":"12","author":"T Tsuchiya","year":"2001","unstructured":"Tsuchiya, T., Nagano, S., Paidi, R.B., Kikuno, T.: Symbolic model checking for self-stabilizing algorithms. IEEE TPDS 12(1), 81\u201395 (2001)","journal-title":"IEEE TPDS"},{"issue":"1","key":"9_CR29","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00446-021-00408-4","volume":"35","author":"M Volk","year":"2022","unstructured":"Volk, M., Bonakdarpour, B., Katoen, J., Aflaki, S.: Synthesizing optimal bias in randomized self-stabilization. Distributed Comput. 35(1), 37\u201357 (2022)","journal-title":"Distributed Comput."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-95497-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T21:43:40Z","timestamp":1757454220000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-95497-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031954962","9783031954979"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-95497-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"11 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"45","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}