K. R. Apt and D. Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, vol.22, issue.6, pp.307-309, 1986.
DOI : 10.1016/0020-0190(86)90071-2

C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain, Certified Impossibility Results for Byzantine-Tolerant Mobile Robots, Proc. of SSS'13, pp.178-186, 2013.
DOI : 10.1007/978-3-319-03089-0_13

URL : https://hal.archives-ouvertes.fr/hal-01126335

T. Balabonski, A. Delga, L. Rieg, S. Tixeuil, and X. Urbain, Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm, Proc. of SSS'16, pp.7-19, 2016.
DOI : 10.1007/978-3-319-25524-8_12

URL : https://hal.archives-ouvertes.fr/hal-01491813

B. Bérard, P. Courtieu, L. Millet, M. Potop-butucaru, L. Rieg et al., Formal Methods for Mobile Robots: Current Results and Open Problems, Int. J. Inform. Soc, vol.7, issue.3, pp.101-114, 2015.

B. Bérard, P. Lafourcade, L. Millet, M. Potop-butucaru, Y. Thierry-mieg et al., Formal verification of mobile robot protocols, Distributed Computing, vol.79, issue.9, 2016.
DOI : 10.1007/s00446-016-0271-1

L. Blin, A. Milani, M. Potop-butucaru, and S. Tixeuil, Exclusive Perpetual Ring Exploration without Chirality, Proc. of DISC'10, pp.312-327, 2010.
DOI : 10.1007/978-3-642-15763-9_29

URL : https://hal.archives-ouvertes.fr/inria-00464206

F. Bonnet, X. Défago, F. Petit, M. Potop-butucaru, and S. Tixeuil, Discovering and Assessing Fine-Grained Metrics in Robot Networks Protocols, 2014 IEEE 33rd International Symposium on Reliable Distributed Systems Workshops, pp.50-59, 2014.
DOI : 10.1109/SRDSW.2014.34

URL : https://hal.archives-ouvertes.fr/hal-00934186

I. Borosh and L. Treybig, Bounds on positive integral solutions of linear Diophantine equations, Proceedings of the American Mathematical Society, vol.55, issue.2, pp.299-304, 1976.
DOI : 10.1090/S0002-9939-1976-0396605-3

P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain, Impossibility of gathering, a certification, Information Processing Letters, vol.115, issue.3, pp.447-452, 2015.
DOI : 10.1016/j.ipl.2014.11.001

URL : https://hal.archives-ouvertes.fr/hal-00995126

P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain, Certified universal gathering in \mathbb R ?2 for oblivious mobile robots, Proc. of DISC'16, pp.187-200, 2016.
DOI : 10.1007/978-3-662-53426-7_14

G. D. Angelo, G. D. Stefano, A. Navarra, N. Nisse, and K. Suchan, A unified approach for different tasks on rings in robot-based computing systems, Proc. of IPDPSW'13, pp.667-676, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00716761

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS'08, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

S. Devismes, A. Lamani, F. Petit, P. Raymond, and S. Tixeuil, Optimal Grid Exploration by Asynchronous Oblivious Robots, Proc. of SSS'12, pp.64-76, 2012.
DOI : 10.1007/978-3-642-33536-5_7

URL : https://hal.archives-ouvertes.fr/hal-00934161

H. T. Doan, F. Bonnet, and K. Ogata, Model Checking of a Mobile Robots Perpetual Exploration Algorithm, Proc. of SOFL+MSVL, Revised Selected Papers, pp.201-219, 2016.
DOI : 10.1007/978-3-662-48653-5_7

P. Flocchini, D. Ilcinkas, A. Pelc, and N. Santoro, Computing Without Communicating: Ring Exploration by Asynchronous Oblivious Robots, Algorithmica, vol.28, issue.3, pp.562-583, 2013.
DOI : 10.1007/s00453-011-9611-5

URL : https://hal.archives-ouvertes.fr/hal-00339884

P. Flocchini, G. Prencipe, and N. Santoro, Distributed Computing by Oblivious Mobile Robots, Synthesis Lectures on Distributed Computing Theory, vol.3, issue.2, 2012.
DOI : 10.2200/S00440ED1V01Y201208DCT010

E. Kranakis, D. Krizanc, and E. Markou, The Mobile Agent Rendezvous Problem in the Ring, Synthesis Lectures on Distributed Computing Theory, vol.1, issue.1, 2010.
DOI : 10.2200/S00278ED1V01Y201004DCT001

R. Mayr, Undecidable problems in unreliable computations, Theoretical Computer Science, vol.297, issue.1-3, pp.337-354, 2003.
DOI : 10.1016/S0304-3975(02)00646-1

L. Millet, M. Potop-butucaru, N. Sznajder, and S. Tixeuil, On the Synthesis of Mobile Robots Algorithms: The Case of Ring Gathering, Proc. of SSS'14, pp.237-251, 2014.
DOI : 10.1007/978-3-319-11764-5_17

URL : https://hal.archives-ouvertes.fr/hal-01016832

M. L. Minsky, Computation: Finite and Infinite Machines, 1967.

S. Rubin, F. Zuleger, A. Murano, and B. Aminof, Verification of asynchronous mobile-robots in partially-known environments, Proc. of PRIMA'15, pp.185-200, 2015.

I. Suzuki and M. Yamashita, Distributed Anonymous Mobile Robots: Formation of Geometric Patterns, SIAM Journal on Computing, vol.28, issue.4, pp.1347-1363, 1999.
DOI : 10.1137/S009753979628292X