{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:17Z","timestamp":1750220657253,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T00:00:00Z","timestamp":1609804800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,1,5]]},"DOI":"10.1145\/3427796.3427832","type":"proceedings-article","created":{"date-parts":[[2020,12,25]],"date-time":"2020-12-25T22:25:45Z","timestamp":1608935145000},"page":"46-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Certification of an Exact Worst-Case Self-Stabilization Time"],"prefix":"10.1145","author":[{"given":"Karine","family":"Altisen","sequence":"first","affiliation":[{"name":"Verimag, FR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Corbineau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, FR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Devismes","sequence":"additional","affiliation":[{"name":"VERIMAG UMR 5104, FR"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,5]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"K. Altisen P. Corbineau and S. Devismes. 2017. A Framework for Certified Self-Stabilization. Logical Methods in Computer Science 13 4 (2017).  K. Altisen P. Corbineau and S. Devismes. 2017. A Framework for Certified Self-Stabilization. Logical Methods in Computer Science 13 4 (2017)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"K. Altisen S. Devismes S. Dubois and F. Petit. 2019. Introduction to Distributed Self-Stabilizing Algorithms. Morgan & Claypool Publishers.  K. Altisen S. Devismes S. Dubois and F. Petit. 2019. Introduction to Distributed Self-Stabilizing Algorithms. Morgan & Claypool Publishers.","DOI":"10.1007\/978-3-031-02013-1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"C. Auger Z. Bouzid P. Courtieu S. Tixeuil and X. Urbain. 2013. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Stabilization Safety and Security of Distributed Systems SSS 2013.  C. Auger Z. Bouzid P. Courtieu S. Tixeuil and X. Urbain. 2013. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Stabilization Safety and Security of Distributed Systems SSS 2013.","DOI":"10.1007\/978-3-319-03089-0_13"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer.  Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_5_1","unstructured":"D. Cansell D. M\u00e9ry and S. Merz. 2001. Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams. In GI Jahrestagung (1). 628\u2013634.  D. Cansell D. M\u00e9ry and S. Merz. 2001. Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams. In GI Jahrestagung (1). 628\u2013634."},{"key":"e_1_3_2_1_6_1","first-page":"39","article-title":"Tasks, Types and Tactics for Local Computation Systems","volume":"9","author":"Cast\u00e9ran Pierre","year":"2011","unstructured":"Pierre Cast\u00e9ran and Vincent Filou . 2011 . Tasks, Types and Tactics for Local Computation Systems . Stud. Inform. Univ. 9 , 1 (2011), 39 \u2013 86 . Pierre Cast\u00e9ran and Vincent Filou. 2011. Tasks, Types and Tactics for Local Computation Systems. Stud. Inform. Univ. 9, 1 (2011), 39\u201386.","journal-title":"Stud. Inform. Univ."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"B. Charron-Bost H. Debrat and S. Merz. 2011. Formal Verification of Consensus Algorithms Tolerating Malicious Faults. In Stabilization Safety and Security of Distributed Systems.  B. Charron-Bost H. Debrat and S. Merz. 2011. Formal Verification of Consensus Algorithms Tolerating Malicious Faults. In Stabilization Safety and Security of Distributed Systems.","DOI":"10.1007\/978-3-642-24550-3_11"},{"key":"e_1_3_2_1_8_1","first-page":"2","article-title":"Formal Verification of a Consensus Algorithm in the Heard-Of","volume":"3","author":"Charron-Bost B.","year":"2009","unstructured":"B. Charron-Bost and S. Merz . 2009 . Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Software and Informatics 3 , 2 - 3 (2009), 273\u2013303. B. Charron-Bost and S. Merz. 2009. Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Software and Informatics 3, 2-3 (2009), 273\u2013303.","journal-title":"Model. Int. J. Software and Informatics"},{"volume-title":"Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS\u201902)","author":"Cournier A.","key":"e_1_3_2_1_9_1","unstructured":"A. Cournier , A.\u00a0 K. Datta , F. Petit , and V. Villain . 2002. Snap-Stabilizing PIF Algorithm in Arbitrary Networks . In Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS\u201902) . 199\u2013206. A. Cournier, A.\u00a0K. Datta, F. Petit, and V. Villain. 2002. Snap-Stabilizing PIF Algorithm in Arbitrary Networks. In Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS\u201902). 199\u2013206."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2002.1016619"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2014.11.001"},{"volume-title":"FM 2012: Formal Methods.","author":"Cousineau D.","key":"e_1_3_2_1_12_1","unstructured":"D. Cousineau , D. Doligez , L. Lamport , S. Merz , D. Ricketts , and H. Vanzetto . 2012. TLA + Proofs . In FM 2012: Formal Methods. D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto. 2012. TLA + Proofs. In FM 2012: Formal Methods."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"C. Delporte-Gallet H. Fauconnier E. Gafni and L. Lamport. 2013. Adaptive Register Allocation with a Linear Number of Registers. In Distributed Computing - 27th International Symposium DISC.  C. Delporte-Gallet H. Fauconnier E. Gafni and L. Lamport. 2013. Adaptive Register Allocation with a Linear Number of Registers. In Distributed Computing - 27th International Symposium DISC.","DOI":"10.1007\/978-3-642-41527-2_19"},{"volume-title":"Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS.","author":"Devismes St\u00e9phane","key":"e_1_3_2_1_14_1","unstructured":"St\u00e9phane Devismes , Anissa Lamani , Franck Petit , Pascal Raymond , and S\u00e9bastien Tixeuil . 2012. Optimal Grid Exploration by Asynchronous Oblivious Robots . In Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS. St\u00e9phane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, and S\u00e9bastien Tixeuil. 2012. Optimal Grid Exploration by Asynchronous Oblivious Robots. In Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/361179.361202"},{"key":"e_1_3_2_1_16_1","volume-title":"Automated Synthesis of Distributed Self-Stabilizing Protocols. Logical Methods in Computer Science 14, 1","author":"Faghih F.","year":"2018","unstructured":"F. Faghih , B. Bonakdarpour , S. Tixeuil , and S.\u00a0 S. Kulkarni . 2018. Automated Synthesis of Distributed Self-Stabilizing Protocols. Logical Methods in Computer Science 14, 1 ( 2018 ). F. Faghih, B. Bonakdarpour, S. Tixeuil, and S.\u00a0S. Kulkarni. 2018. Automated Synthesis of Distributed Self-Stabilizing Protocols. Logical Methods in Computer Science 14, 1 (2018)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1195881.1195883"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050035"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.003"},{"key":"e_1_3_2_1_20_1","volume-title":"Proving the Correctness of Disk Paxos. Archive of Formal Proofs 2005","author":"Jaskelioff Mauro","year":"2005","unstructured":"Mauro Jaskelioff and Stephan Merz . 2005. Proving the Correctness of Disk Paxos. Archive of Formal Proofs 2005 ( 2005 ). Mauro Jaskelioff and Stephan Merz. 2005. Proving the Correctness of Disk Paxos. Archive of Formal Proofs 2005 (2005)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"M. Kimoto T. Tsuchiya and T. Kikuno. 2009. On the Time Complexity of Dijkstra\u2019s Three-State Mutual Exclusion Algorithm. IEICE Transactions 92-D(2009) 1570\u20131573.  M. Kimoto T. Tsuchiya and T. Kikuno. 2009. On the Time Complexity of Dijkstra\u2019s Three-State Mutual Exclusion Algorithm. IEICE Transactions 92-D(2009) 1570\u20131573.","DOI":"10.1587\/transinf.E92.D.1570"},{"key":"e_1_3_2_1_22_1","unstructured":"P. K\u00fcfner U. Nestmann and C. Rickmann. 2012. Formal Verification of Distributed Algorithms - From Pseudo Code to Checked Proofs. In Theoretical Computer Science - 7th IFIP TC 1\/WG 2.2 International Conference TCS.  P. K\u00fcfner U. Nestmann and C. Rickmann. 2012. Formal Verification of Distributed Algorithms - From Pseudo Code to Checked Proofs. In Theoretical Computer Science - 7th IFIP TC 1\/WG 2.2 International Conference TCS."},{"volume-title":"19th IEEE International Conference on Distributed Computing Systems.","author":"Kulkarni S.","key":"e_1_3_2_1_23_1","unstructured":"S.\u00a0 S. Kulkarni , J. Rushby , and N. Shankar . 1999. A case-study in component-based mechanical verification of fault-tolerant programs . In 19th IEEE International Conference on Distributed Computing Systems. S.\u00a0S. Kulkarni, J. Rushby, and N. Shankar. 1999. A case-study in component-based mechanical verification of fault-tolerant programs. In 19th IEEE International Conference on Distributed Computing Systems."},{"key":"e_1_3_2_1_24_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA."},{"volume-title":"International Conference on Programming Concepts and Methods (PROCOMET \u201998)","author":"Qadeer S.","key":"e_1_3_2_1_26_1","unstructured":"S. Qadeer and N. Shankar . 1998. Verifying a Self-Stabilizing Mutual Exclusion Algorithm . In International Conference on Programming Concepts and Methods (PROCOMET \u201998) . S. Qadeer and N. Shankar. 1998. Verifying a Self-Stabilizing Mutual Exclusion Algorithm. In International Conference on Programming Concepts and Methods (PROCOMET \u201998)."},{"key":"e_1_3_2_1_27_1","unstructured":"V. Rahli D. Guaspari M. Bickford and R.\u00a0L. Constable. 2015. Formal Specification Verification and Implementation of Fault-Tolerant Systems using EventML. ECEASST 72(2015).  V. Rahli D. Guaspari M. Bickford and R.\u00a0L. Constable. 2015. Formal Specification Verification and Implementation of Fault-Tolerant Systems using EventML. ECEASST 72(2015)."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.009"},{"key":"e_1_3_2_1_29_1","volume-title":"Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP.","author":"Rahli V.","year":"2018","unstructured":"V. Rahli , I. Vukotic , M. V\u00f6lp , and P.\u00a0J.\u00a0 Esteves Ver\u00edssimo . 2018 . Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP. V. Rahli, I. Vukotic, M. V\u00f6lp, and P.\u00a0J.\u00a0Esteves Ver\u00edssimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP."},{"key":"e_1_3_2_1_30_1","unstructured":"S\u00e9bastien Tixeuil. 2006. Toward self-stabilizing large-scale systems. Habilitation \u00e0 diriger des recherches. Universit\u00e9 Paris Sud - Paris XI.  S\u00e9bastien Tixeuil. 2006. Toward self-stabilizing large-scale systems. Habilitation \u00e0 diriger des recherches. Universit\u00e9 Paris Sud - Paris XI."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.899941"}],"event":{"name":"ICDCN '21: International Conference on Distributed Computing and Networking 2021","acronym":"ICDCN '21","location":"Nara Japan"},"container-title":["Proceedings of the 22nd International Conference on Distributed Computing and Networking"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427796.3427832","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427796.3427832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:32Z","timestamp":1750197752000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427796.3427832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,5]]},"references-count":30,"alternative-id":["10.1145\/3427796.3427832","10.1145\/3427796"],"URL":"https:\/\/doi.org\/10.1145\/3427796.3427832","relation":{},"subject":[],"published":{"date-parts":[[2021,1,5]]},"assertion":[{"value":"2021-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}