{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T06:05:04Z","timestamp":1779602704463,"version":"3.53.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032264640","type":"print"},{"value":"9783032264657","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-26465-7_3","type":"book-chapter","created":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T05:49:21Z","timestamp":1779601761000},"page":"34-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Certification of\u00a0async Protocols: The\u00a0Case of\u00a0Gathering in\u00a0$$\\mathbb {R} ^2$$ Using Weber Points"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4428-065X","authenticated-orcid":false,"given":"Maria-Virginia","family":"Aponte","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7817-9551","authenticated-orcid":false,"given":"Mathis","family":"Bouverot-Dupuis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0612-5616","authenticated-orcid":false,"given":"Quentin","family":"Bramas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8789-9781","authenticated-orcid":false,"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5751-3806","authenticated-orcid":false,"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7442-2538","authenticated-orcid":false,"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,24]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings. LNCSvol.\u00a09688, pp. 36\u201351. Springer-Verlag (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_3","DOI":"10.1007\/978-3-319-39570-8_3"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. Theory Comput. Syst., 200\u2013218 (2019). https:\/\/doi.org\/10.1007\/s00224-017-9828-z","DOI":"10.1007\/s00224-017-9828-z"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Balabonski, T., Pelle, R., Rieg, L., Tixeuil, S.: A foundational framework for certified impossibility results with mobile robots on graphs. In: Bellavista, P., Garg, V.K. (eds.) Proceedings of the 19th International Conference on Distributed Computing and Networking, ICDCN 2018, Varanasi, India, January 4-7, 2018, pp. 5:1\u20135:10. ACM (2018). https:\/\/doi.org\/10.1145\/3154273.3154321","DOI":"10.1145\/3154273.3154321"},{"key":"3_CR4","unstructured":"Bauer, A.: How to review formalized mathematics. Blog post (2013). http:\/\/math.andrej.com\/2013\/08\/19\/how-to-review-formalized-mathematics\/"},{"issue":"6","key":"3_CR5","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00446-016-0271-1","volume":"29","author":"B B\u00e9rard","year":"2016","unstructured":"B\u00e9rard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Distrib. Comput. 29(6), 459\u2013487 (2016). https:\/\/doi.org\/10.1007\/s00446-016-0271-1","journal-title":"Distrib. Comput."},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01212523","volume":"9","author":"M Bezem","year":"1997","unstructured":"Bezem, M., Bol, R., Groote, J.F.: Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects Comput. 9, 1\u201348 (1997)","journal-title":"Formal Aspects Comput."},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Bonnet, F., et al.: Deterministic color-optimal self-stabilizing semi-synchronous gathering: a certified algorithm. In: Schmid, U., Kuznets, R. (eds.) Structural Information and Communication Complexity - 32nd International Colloquium (SIROCCO 2025). LNCS, vol. 15671, pp. 127\u2013143. Springer Nature Switzerland, Delphi, Greece (2025). https:\/\/doi.org\/10.1007\/978-3-031-91736-3_8, https:\/\/hal.science\/hal-04988128","DOI":"10.1007\/978-3-031-91736-3_8"},{"key":"3_CR8","unstructured":"Bouzid, Z.: Mod\u00e8les et algorithmes pour les syst\u00e8mes \u00e9mergents. Ph.D. thesis, Universit\u00e9 Pierre et Marie Curie, Paris, France (2013)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cicerone, S., Stefano, G.D., Navarra, A.: Gathering of robots on meeting-points: feasibility and optimal resolution algorithms. Distrib. Comput. 31, 1\u201350 (2018). https:\/\/api.semanticscholar.org\/CorpusID:861053","DOI":"10.1007\/s00446-017-0293-3"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Cieliebak, M., Flocchini, P., Prencipe, G., Santoro, N.: Distributed computing by mobile robots: gathering. SIAM J. Comput. 41(4), 829\u2013879 (2012). https:\/\/doi.org\/10.1137\/100796534","DOI":"10.1137\/100796534"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Swarms of mobile robots: towards versatility with safety. Leibniz Trans. Embed. Syst. 8(2), 02:1\u201302:36 (2022). https:\/\/doi.org\/10.4230\/LITES.8.2.2, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LITES.8.2.2","DOI":"10.4230\/LITES.8.2.2"},{"key":"3_CR12","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, 447\u2013452 (2015). https:\/\/doi.org\/10.1016\/j.ipl.2014.11.001","journal-title":"Inf. Process. Lett."},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering algorithm in $$\\mathbb{R}^2$$ for oblivious mobile robots. In: Gavoille, C., Ilcinkas, D. (eds.) Distributed Computing - 30th International Symposium, (DISC 2016). LeNCS, vol.\u00a09888, pp. 187\u2013200. Springer-Verlag, Paris, France (2016). https:\/\/doi.org\/10.1007\/978-3-662-53426-7_14","DOI":"10.1007\/978-3-662-53426-7_14"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-642-32759-9_14","volume-title":"FM","author":"D Cousineau","year":"2012","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM. Lecture Notes in Computer Science, vol. 7436, pp. 147\u2013154. Springer-Verlag, Paris, France (Aug (2012)"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"D\u00e9fago, X., Heriban, A., Tixeuil, S., Wada, K.: Using model checking to formally verify rendezvous algorithms for robots with lights in euclidean space. In: International Symposium on Reliable Distributed Systems, SRDS 2020, Shanghai, China, September 21-24, 2020, pp. 113\u2013122. IEEE (2020). https:\/\/doi.org\/10.1109\/SRDS51746.2020.00019","DOI":"10.1109\/SRDS51746.2020.00019"},{"key":"3_CR16","first-page":"201","volume-title":"Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009)","author":"Y Deng","year":"2009","unstructured":"Deng, Y., Monin, J.F.: Verifying self-stabilizing population protocols with COQ. In: Chin, W.N., Qin, S. (eds.) Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pp. 201\u2013208. IEEE Computer Society, Tianjin, China (Jul (2009)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-33536-5_7","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"S Devismes","year":"2012","unstructured":"Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 64\u201376. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33536-5_7"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of a mobile robots perpetual exploration algorithm. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds.) Structured Object-Oriented Formal Language and Method - 6th International Workshop, SOFL+MSVL 2016, Tokyo, Japan, November 15, 2016, Revised Selected Papers. LNCS, vol. 10189, pp. 201\u2013219 (2016). https:\/\/doi.org\/10.1007\/978-3-319-57708-1_12","DOI":"10.1007\/978-3-319-57708-1_12"},{"key":"3_CR19","unstructured":"Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Felber, P. (eds.) Principles of Distributed Systems - 21st International Conference (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Lisbon, Portugal (2017)"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Fokkink, W.: Modelling Distributed Systems. EATCS Texts in Theoretical Computer Science, Springer-Verlag (2007). https:\/\/doi.org\/10.1007\/978-3-540-73938-8","DOI":"10.1007\/978-3-540-73938-8"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Frei, F., Wada, K.: Invited paper: gathering oblivious robots in the plane. In: Stabilization, Safety, and Security of Distributed Systems: 26th International Symposium, SSS 2024, Nagoya, Japan, October 20\u201322, 2024, Proceedings, pp. 39\u201354. Springer-Verlag, Berlin, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-74498-3_3","DOI":"10.1007\/978-3-031-74498-3_3"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Gaspar, N., Henrio, L., Madelaine, E.: Bringing COQ into the world of GCM distributed applications. Int. J. Parallel Programm. 42(4), 643\u2013662 (2014)","DOI":"10.1007\/s10766-013-0264-7"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-33475-7_15","volume-title":"Theoretical Computer Science","author":"P K\u00fcfner","year":"2012","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., 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"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-58468-4_159","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"L Lamport","year":"1994","unstructured":"Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 41\u201376. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58468-4_159"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE. LNCS, vol.\u00a09195, pp. 378\u2013388. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6, http:\/\/dblp.uni-trier.de\/db\/conf\/cade\/cade2015.html#MouraKADR15","DOI":"10.1007\/978-3-319-21401-6"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 a proof assistant for higher-order logic, LNCS, vol.\u00a02283. Springer-Verlag (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Potop-Butucaru, M., Sznajder, N., Tixeuil, S., Urbain, X.: Formal methods for mobile robots. In: Flocchini, P., Prencipe, G., Santoro, N. (eds.) Distributed Computing by Mobile Entities, Current Research in Moving and Computing, LNCS, vol. 11340, pp. 278\u2013313. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-11072-7_12","DOI":"10.1007\/978-3-030-11072-7_12"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods Syst. Des. 56(1), 55\u201389 (2020). https:\/\/doi.org\/10.1007\/s10703-019-00335-y","DOI":"10.1007\/s10703-019-00335-y"},{"issue":"4","key":"3_CR29","doi-asserted-by":"publisher","first-page":"1347","DOI":"10.1137\/S009753979628292X","volume":"28","author":"I Suzuki","year":"1999","unstructured":"Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347\u20131363 (1999)","journal-title":"SIAM J. Comput."},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Team, T.C.D.: The COQ proof assistant. Tech. rep. (2024). https:\/\/doi.org\/10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"}],"container-title":["Lecture Notes in Computer Science","Structural Information and Communication Complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26465-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T05:49:24Z","timestamp":1779601764000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26465-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032264640","9783032264657"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26465-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of interest"}},{"value":"SIROCCO","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Structural Information and Communication Complexity","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Durham","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sirocco2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sirocco2026.webspace.durham.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}