{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:01:17Z","timestamp":1758272477776,"version":"3.40.3"},"publisher-location":"Cham","reference-count":76,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030110710"},{"type":"electronic","value":"9783030110727"}],"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-11072-7_12","type":"book-chapter","created":{"date-parts":[[2019,1,12]],"date-time":"2019-01-12T08:03:00Z","timestamp":1547280180000},"page":"278-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Methods for Mobile Robots"],"prefix":"10.1007","author":[{"given":"Maria","family":"Potop-Butucaru","sequence":"first","affiliation":[]},{"given":"Nathalie","family":"Sznajder","sequence":"additional","affiliation":[]},{"given":"S\u00e9bastien","family":"Tixeuil","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,1,13]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1\u201317. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035748"},{"key":"12_CR2","unstructured":"ACL2. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"key":"12_CR3","unstructured":"Agda. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bacelar Almeida, J., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Zanella B\u00e9guelin, S.: Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) ACM Conference on Computer and Communications Security, pp. 488\u2013500. ACM (2012)","DOI":"10.1145\/2382196.2382249"},{"key":"12_CR5","unstructured":"Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Automatic verification of multi-agent systems in parameterised grid-environments. In: Jonker, C.M., Marsella, S., Thangarajah, J., Tuyls, K. (eds.) Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, 9\u201313 May 2016, pp. 1190\u20131199. ACM (2016)"},{"issue":"6","key":"12_CR6","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_19"},{"key":"12_CR8","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":"12_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03232-6_29","volume-title":"Stabilization, Safety, and Security of Distributed Systems - 20th International Symposium, (SSS 2018)","author":"T Balabonski","year":"2018","unstructured":"Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Brief announcement: continuous vs. discrete asynchronous moves: a certified approach for mobile robots. In: Izumi, T., Kuznetsov, P. (eds.) SSS 2018. LNCS. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-03232-6_29"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Continuous vs. discrete asynchronous moves: a certified approach for mobile robots. Research report, Sorbonne Universit\u00e9, CNRS, Laboratoire d\u2019Informatique de Paris 6, LIP6, F-75005 Paris, France (2018)","DOI":"10.1007\/978-3-030-03232-6_29"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-319-67113-0_11","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"T Balabonski","year":"2017","unstructured":"Balabonski, T., Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified gathering of oblivious mobile robots: survey of recent results and open problems. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS\/AVoCS -2017. LNCS, vol. 10471, pp. 165\u2013181. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67113-0_11"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. ACM Trans. Comput. Syst. (2018). https:\/\/doi.org\/10.1007\/s00224-017-9828-z","DOI":"10.1007\/s00224-017-9828-z"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Balabonski, T., Pelle, R., Rieg, L., Tixeuil, S.: A foundational framework for certified impossibility results with mobile robots on graphs. In: Proceedings of International Conference on Distributed Computing and Networking, Varanasi, India, January 2018","DOI":"10.1145\/3154273.3154321"},{"issue":"6","key":"12_CR15","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)","journal-title":"Distrib. Comput."},{"key":"12_CR16","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. Form. Asp. Comput. 9, 1\u201348 (1997)","journal-title":"Form. Asp. Comput."},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-61474-5_92","volume-title":"Computer Aided Verification","author":"N Bj\u00f8rner","year":"1996","unstructured":"Bj\u00f8rner, N., et al.: STeP: deductive-algorithmic verification of reactive and real-time systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 415\u2013418. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_92"},{"key":"12_CR18","first-page":"282","volume-title":"Lecture Notes in Computer Science","author":"Fran\u00e7ois Bonnet","year":"2012","unstructured":"Bonnet, F., D\u00e9fago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Brief announcement: discovering and assessing fine-grained metrics in robot networks protocols. In: Richa and Scheideler [71], pp. 282\u2013284 (2012)"},{"key":"12_CR19","doi-asserted-by":"crossref","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 Computer Society (2014)","DOI":"10.1109\/SRDSW.2014.34"},{"issue":"34\u201336","key":"12_CR20","doi-asserted-by":"publisher","first-page":"3154","DOI":"10.1016\/j.tcs.2010.05.006","volume":"411","author":"Z Bouzid","year":"2010","unstructured":"Bouzid, Z., Potop-Butucaru, M.G., Tixeuil, S.: Optimal byzantine-resilient convergence in uni-dimensional robot networks. Theor. Comput. Sci. 411(34\u201336), 3154\u20133168 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR21","volume-title":"A Computational Logic Handbook","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, Cambridge (1988)"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-74107-7_3","volume-title":"Logics of Specification Languages","author":"D Cansell","year":"2007","unstructured":"Cansell, D., M\u00e9ry, D.: The event-B modelling method: concepts and case studies. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages, pp. 47\u2013152. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74107-7_3"},{"issue":"2","key":"12_CR24","first-page":"159","volume":"7","author":"D Cansell","year":"2001","unstructured":"Cansell, D., M\u00e9ry, D., Merz, S.: Diagram refinements for the design of reactive systems. J. Univ. Comp. Sci. 7(2), 159\u2013174 (2001)","journal-title":"J. Univ. Comp. Sci."},{"key":"12_CR25","unstructured":"Cast\u00e9ran, P., Filou, V., Mosbah, M.: Certifying distributed algorithms by embedding local computation systems in the Coq proof assistant. In: Bouhoula, A., Ida, T. (eds.) Symbolic Computation in Software Science (SCSS 2009) (2009)"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-24550-3_11","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"B Charron-Bost","year":"2011","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"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-16023-3_19","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"I Chatzigiannakis","year":"2010","unstructured":"Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Algorithmic verification of population protocols. In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds.) SSS 2010. LNCS, vol. 6366, pp. 221\u2013235. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16023-3_19"},{"key":"12_CR28","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1093\/comjnl\/38.2.152","volume":"38","author":"C-T Chou","year":"1995","unstructured":"Chou, C.-T.: Mechanical verification of distributed algorithms in higher-order logic. Comput. J. 38, 158\u2013176 (1995)","journal-title":"Comput. J."},{"key":"12_CR29","unstructured":"Church, A.: Logic, arithmetics, and automata. In: Proceedings of International Congress of Mathematicians, pp. 23\u201335 (1963)"},{"key":"12_CR30","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of IBM Workshop on Logics of Programs (1981)"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume-title":"CONCUR \u201995: Concurrency Theory","author":"EM Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395\u2013407. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_30"},{"key":"12_CR32","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: Distributed Computing Systems, pp. 215\u2013224. IEEE (2011)","DOI":"10.1109\/ICDCS.2011.36"},{"issue":"6","key":"12_CR34","doi-asserted-by":"publisher","first-page":"1516","DOI":"10.1137\/S0097539704446475","volume":"34","author":"R Cohen","year":"2005","unstructured":"Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516\u20131528 (2005)","journal-title":"SIAM J. Comput."},{"key":"12_CR35","unstructured":"Coq. https:\/\/coq.inria.fr\/"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG 1988","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_47"},{"key":"12_CR37","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. CoRR, abs\/1506.01603 (2015)"},{"key":"12_CR38","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)","journal-title":"Inf. Process. Lett."},{"key":"12_CR39","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":"12_CR40","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":"12_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/BFb0035398","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Alfaro","year":"1997","unstructured":"de Alfaro, L., Manna, Z., Sipma, H.B., Uribe, T.E.: Visual verification of reactive systems. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 334\u2013350. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0035398"},{"key":"12_CR42","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":"12_CR43","first-page":"64","volume-title":"Lecture Notes in Computer Science","author":"St\u00e9phane Devismes","year":"2012","unstructured":"Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Richa and Scheideler [71], pp. 64\u201376 (2012)"},{"key":"12_CR44","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":"12_CR45","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, volume 95 of LIPIcs, pp. 12:1\u201312:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"12_CR46","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual Symposium on Logic in Computer Science, pp. 352\u2013359. IEEE (1999)"},{"key":"12_CR47","doi-asserted-by":"publisher","DOI":"10.2200\/S00440ED1V01Y201208DCT010","volume-title":"Distributed Computing by Oblivious Mobile Robots","author":"P Flocchini","year":"2012","unstructured":"Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Morgan & Claypool Publishers, San Rafael (2012)"},{"key":"12_CR48","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73938-8","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). https:\/\/doi.org\/10.1007\/978-3-540-73938-8"},{"issue":"1","key":"12_CR49","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1142\/S0129626403001094","volume":"13","author":"E Gascard","year":"2003","unstructured":"Gascard, E., Pierre, L.: Formal proof of applications distributed in symmetric interconnexion networks. Parallel Process. Lett. 13(1), 3\u201318 (2003)","journal-title":"Parallel Process. Lett."},{"key":"12_CR50","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. In: Notices of the AMS, vol. 55, p. 1370, December 2008"},{"key":"12_CR51","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 1\u20132. ACM (2013)","DOI":"10.1145\/2480359.2429071"},{"key":"12_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"issue":"3","key":"12_CR53","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s00446-009-0092-6","volume":"22","author":"Rachid Guerraoui","year":"2009","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput., 129\u2013145 (2010)","journal-title":"Distributed Computing"},{"issue":"9","key":"12_CR54","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"issue":"6","key":"12_CR55","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., et al.: seL4: formal verification of an operating system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"12_CR56","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":"12_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11506676_3","volume-title":"Logic Based Program Synthesis and Transformation","author":"SS Kulkarni","year":"2005","unstructured":"Kulkarni, S.S., Bonakdarpour, B., Ebnenasir, A.: Mechanical verification of automatic synthesis of fault-tolerant programs. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 36\u201352. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11506676_3"},{"key":"12_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-24100-0_22","volume-title":"Distributed Computing","author":"L Lamport","year":"2011","unstructured":"Lamport, L.: Byzantizing paxos by refinement. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 211\u2013224. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24100-0_22"},{"key":"12_CR59","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"},{"issue":"3","key":"12_CR60","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"12_CR61","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"12_CR62","unstructured":"Loco. http:\/\/www.labri.fr\/~casteran\/Loco"},{"key":"12_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-21461-5_16","volume-title":"Formal Techniques for Distributed Systems","author":"T Lu","year":"2011","unstructured":"Lu, T., Merz, S., Weidenbach, C.: Towards verification of the pastry protocol using TLA$$^{+}$$. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE -2011. LNCS, vol. 6722, pp. 244\u2013258. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_16"},{"key":"12_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1007\/3-540-57887-0_123","volume-title":"Theoretical Aspects of Computer Software","author":"Z Manna","year":"1994","unstructured":"Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 726\u2013765. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_123"},{"issue":"1","key":"12_CR65","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR66","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":"12_CR67","unstructured":"Mizar. http:\/\/mizar.uwb.edu.pl\/"},{"key":"12_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"12_CR69","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL 1989, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"key":"12_CR70","unstructured":"PVS. http:\/\/pvs.csl.sri.com\/"},{"key":"12_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33536-5","volume-title":"Stabilization, Safety, and Security of Distributed Systems","year":"2012","unstructured":"Richa, A.W., Scheideler, C. (eds.): SSS 2012. LNCS, vol. 7596. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33536-5"},{"key":"12_CR72","doi-asserted-by":"crossref","unstructured":"Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 212\u2013219. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102262"},{"issue":"4","key":"12_CR73","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":"12_CR74","unstructured":"Flyspeck Development Team. The Flyspeck Project. https:\/\/code.google.com\/p\/flyspeck\/"},{"key":"12_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-74591-4_24","volume-title":"Theorem Proving in Higher Order Logics","author":"L Th\u00e9ry","year":"2007","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 319\u2013333. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_24"},{"key":"12_CR76","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s00446-010-0123-3","volume":"23","author":"T Tsuchiya","year":"2011","unstructured":"Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrib. Comput. 23, 341\u2013358 (2011)","journal-title":"Distrib. Comput."}],"container-title":["Lecture Notes in Computer Science","Distributed Computing by Mobile Entities"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11072-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T13:26:11Z","timestamp":1710249971000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-11072-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030110710","9783030110727"],"references-count":76,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11072-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"13 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}