{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:09Z","timestamp":1760202669230,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030883"},{"type":"electronic","value":"9783319030890"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03089-0_13","type":"book-chapter","created":{"date-parts":[[2013,10,17]],"date-time":"2013-10-17T15:18:14Z","timestamp":1382023094000},"page":"178-190","source":"Crossref","is-referenced-by-count":31,"title":["Certified Impossibility Results for Byzantine-Tolerant Mobile Robots"],"prefix":"10.1007","author":[{"given":"C\u00e9dric","family":"Auger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohir","family":"Bouzid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Courtieu","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","reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1137\/050645221","volume":"36","author":"N. Agmon","year":"2006","unstructured":"Agmon, N., Peleg, D.: Fault-tolerant gathering algorithms for autonomous mobile robots. SIAM Journal on Computing\u00a036(1), 56\u201382 (2006)","journal-title":"SIAM Journal on Computing"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., B\u00e9guelin, S.Z.: 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":"13_CR3","unstructured":"Berard, B., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of Mobile Robot Protocols. Technical report (May 2013)"},{"key":"13_CR4","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 of Computing\u00a09, 1\u201348 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-33536-5_28","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"F. Bonnet","year":"2012","unstructured":"Bonnet, F., D\u00e9fago, X., Petit, F., Potop-Butucaru, M.G., Tixeuil, S.: Brief Announcement: Discovering and Assessing Fine-Grained Metrics in Robot Networks Protocols. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol.\u00a07596, pp. 282\u2013284. Springer, Heidelberg (2012)"},{"issue":"34-36","key":"13_CR6","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. Theoretical Computer Science\u00a0411(34-36), 3154\u20133168 (2010)","journal-title":"Theoretical Computer Science"},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.entcs.2007.05.027","volume":"185","author":"M. Cadilhac","year":"2007","unstructured":"Cadilhac, M., H\u00e9rault, T., Lassaigne, R., Peyronnet, S., Tixeuil, S.: Evaluating complex MAC protocols for sensor networks with APMC. Electronic Notes in Theoretical Computer Science\u00a0185, 33\u201346 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Cansell, D., M\u00e9ry, D.: The Event-B Modelling Method: Concepts and Case Studies. In: Logics of Specification Languages, pp. 47\u2013152. Springer (2007)","DOI":"10.1007\/978-3-540-74107-7_3"},{"key":"13_CR9","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":"13_CR10","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. The Computer Journal\u00a038, 158\u2013176 (1995)","journal-title":"The Computer Journal"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: ICDCS, Minneapolis, Minnesota, USA, pp. 215\u2013224. IEEE Computer Society (June 2011)","DOI":"10.1109\/ICDCS.2011.36"},{"key":"13_CR12","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-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively Defined Types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"13_CR13","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.\u00a07436, pp. 147\u2013154. Springer, Heidelberg (2012)"},{"key":"13_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":"13_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.\u00a07596, pp. 64\u201376. Springer, Heidelberg (2012)"},{"key":"13_CR16","unstructured":"Dubois, S., Tixeuil, S.: A Taxonomy of Daemons in Self-stabilization. Technical Report 1110.0334, ArXiv eprint (October 2011)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Fellahi, N., Bonakdarpour, B., Tixeuil, S.: Rigorous performance evaluation of self-stabilization using probabilistic model checking. In: Proceedings of the International Conference on Reliable Distributed Systems (SRDS 2013), Braga, Portugal. IEEE Computer Society (September 2013)","DOI":"10.1109\/SRDS.2013.24"},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M.J. Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of Distributed Consensus with One Faulty Process. J. ACM\u00a032(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2012)","DOI":"10.2200\/S00440ED1V01Y201208DCT010"},{"key":"13_CR20","unstructured":"Fokkink, W.: Modelling Distributed Systems. EATCS Texts in Theoretical Computer Science. Springer (2007)"},{"key":"13_CR21","first-page":"1370","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal\u2013Proof The Four-Color Theorem. Notices of the AMS\u00a055, 1370 (2008)","journal-title":"Notices of the AMS"},{"key":"13_CR22","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":"13_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.\u00a07604, pp. 209\u2013224. Springer, Heidelberg (2012)"},{"key":"13_CR24","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 2001. LNCS, vol.\u00a06950, pp. 211\u2013224. Springer, Heidelberg (2011)"},{"issue":"3","key":"13_CR25","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 Transactions on Programming Languages and Systems\u00a04(3), 382\u2013401 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"13_CR26","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. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Litovsky, I., M\u00e9tivier, Y., Sopena, \u00c9.: Graph Relabelling Systems and Distributed Algorithms. In: Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, vol.\u00a03, pp. 1\u201356. World Scientific (1999)","DOI":"10.1142\/9789812814951_0001"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Mccarthy, J., Painter, J.: Correctness of a Compiler for Arithmetic Expressions. In: Proceedings of Applied Mathematica. Mathematical Aspects of Computer Science, vol.\u00a019, pp. 33\u201341. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"issue":"2","key":"13_CR29","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M.C. Pease","year":"1980","unstructured":"Pease, M.C., Shostak, R.E., Lamport, L.: Reaching Agreement in the Presence of Faults. J. ACM\u00a027(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"13_CR30","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 Journal of Computing\u00a028(4), 1347\u20131363 (1999)","journal-title":"SIAM Journal of Computing"},{"key":"13_CR31","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.\u00a04732, pp. 319\u2013333. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Stabilization, Safety, and Security of Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03089-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T17:25:55Z","timestamp":1746033955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03089-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030883","9783319030890"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03089-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}