{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:56:05Z","timestamp":1742986565547,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030910808"},{"type":"electronic","value":"9783030910815"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91081-5_31","type":"book-chapter","created":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T21:03:40Z","timestamp":1636405420000},"page":"469-473","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Computer Aided Formal Design of Swarm Robotics Algorithms"],"prefix":"10.1007","author":[{"given":"Thibaut","family":"Balabonski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robin","family":"Pelle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Tixeuil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,9]]},"reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-319-39570-8_3","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"K Altisen","year":"2016","unstructured":"Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 36\u201351. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_3"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-03089-0_13","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"C Auger","year":"2013","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"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-31277-0_7","volume-title":"Networked Systems","author":"T Balabonski","year":"2019","unstructured":"Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Continuous vs. discrete asynchronous moves: a certified approach for mobile robots. In: Atig, M.F., Schwarzmann, A.A. (eds.) NETYS 2019. LNCS, vol. 11704, pp. 93\u2013109. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31277-0_7"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Computer aided formal design of swarm robotics algorithms. CoRR abs\/2101.06966 (2021). https:\/\/arxiv.org\/abs\/2101.06966","DOI":"10.1007\/978-3-030-91081-5_31"},{"issue":"2","key":"31_CR5","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/s00224-017-9828-z","volume":"63","author":"T Balabonski","year":"2017","unstructured":"Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. Theory Comput. Syst. 63(2), 200\u2013218 (2017). https:\/\/doi.org\/10.1007\/s00224-017-9828-z","journal-title":"Theory Comput. Syst."},{"key":"31_CR6","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, 4\u20137 January 2018, pp. 5:1\u20135:10. ACM (2018). https:\/\/doi.org\/10.1145\/3154273.3154321","DOI":"10.1145\/3154273.3154321"},{"issue":"6","key":"31_CR7","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":"31_CR8","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":"31_CR9","doi-asserted-by":"publisher","unstructured":"Bonnet, F., D\u00e9fago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Discovering and assessing fine-grained metrics in robot networks protocols. In: 33rd IEEE International Symposium on Reliable Distributed Systems Workshops, SRDS Workshops 2014, Nara, Japan, 6\u20139 October 2014, pp. 50\u201359. IEEE (2014). https:\/\/doi.org\/10.1109\/SRDSW.2014.34","DOI":"10.1109\/SRDSW.2014.34"},{"key":"31_CR10","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":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-662-53426-7_14","volume-title":"Distributed Computing","author":"P Courtieu","year":"2016","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering in $$\\mathbb{R}^2$$ for oblivious mobile robots. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 187\u2013200. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53426-7_14"},{"key":"31_CR12","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$$^{+}$$ Proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147\u2013154. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_14"},{"key":"31_CR13","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, 21\u201324 September 2020, pp. 113\u2013122. IEEE (2020). https:\/\/doi.org\/10.1109\/SRDS51746.2020.00019","DOI":"10.1109\/SRDS51746.2020.00019"},{"key":"31_CR14","doi-asserted-by":"crossref","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), Tianjin, China, pp. 201\u2013208. IEEE Computer Society, July 2009","DOI":"10.1109\/TASE.2009.9"},{"key":"31_CR15","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":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-57708-1_12","volume-title":"Structured Object-Oriented Formal Language and Method","author":"HTT Doan","year":"2017","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.) SOFL+MSVL 2016. LNCS, vol. 10189, pp. 201\u2013219. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57708-1_12"},{"key":"31_CR17","doi-asserted-by":"publisher","unstructured":"Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Bessani, A., Felber, P., Leit\u00e3o, J. (eds.) 21st International Conference on Principles of Distributed Systems, OPODIS 2017, Lisbon, Portugal, 18\u201320 December 2017. LIPIcs, vol. 95, pp. 12:1\u201312:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2017.12","DOI":"10.4230\/LIPIcs.OPODIS.2017.12"},{"issue":"1\u20133","key":"31_CR18","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.tcs.2005.01.001","volume":"337","author":"P Flocchini","year":"2005","unstructured":"Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Gathering of asynchronous robots with limited visibility. Theor. Comput. Sci. 337(1\u20133), 147\u2013168 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2005.01.001","journal-title":"Theor. Comput. Sci."},{"key":"31_CR19","series-title":"EATCS Texts in Theoretical Computer Science","volume-title":"Modelling Distributed Systems","author":"W Fokkink","year":"2007","unstructured":"Fokkink, W.: Modelling Distributed Systems. EATCS Texts in Theoretical Computer Science, Springer, Heidelberg (2007)"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Gaspar, N., Henrio, L., Madelaine, E.: Bringing coq into the world of GCM distributed applications, pp. 643\u2013662 (2014)","DOI":"10.1007\/s10766-013-0264-7"},{"key":"31_CR21","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"},{"issue":"3","key":"31_CR22","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). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-11764-5_17","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"L Millet","year":"2014","unstructured":"Millet, L., Potop-Butucaru, M., Sznajder, N., Tixeuil, S.: On the synthesis of mobile robots algorithms: the case of ring gathering. In: Felber, P., Garg, V. (eds.) SSS 2014. LNCS, vol. 8756, pp. 237\u2013251. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11764-5_17"},{"key":"31_CR24","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. (6), 55\u201389 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00335-y","DOI":"10.1007\/s10703-019-00335-y"},{"issue":"4","key":"31_CR25","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."}],"container-title":["Lecture Notes in Computer Science","Stabilization, Safety, and Security of Distributed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91081-5_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T15:43:22Z","timestamp":1710258202000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91081-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030910808","9783030910815"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91081-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"9 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Stabilizing, Safety, and Security of Distributed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sss2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cse.chalmers.se\/~elad\/SSS2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"56","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":"16","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":"10","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":"29% - 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","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)"}}]}}