[CUT16a] Certified Universal Gathering in {\textbackslash}mathbb {R} {\^{}}2 for Oblivious Mobile Robots

Conférence Internationale avec comité de lecture : DISC 2016, Distributed Computing 30th International Symposium, September 2016, Vol. 9888, pp.187-200, Series LNCS, Paris, France, (DOI: 10.1007/978-3-662-53426-7_14)

Auteurs: P. Courtieu , X. Urbain , S. Tixeuil , L. Rieg

Mots clés: Distributed algorithm, Robot swarm, formal proof, proof assistant

Résumé: A formal proof, in the Coq proof assistant, of a distributed algorithm for robot gathering. Robots are oblivious, semi-synchronized, and cannot communicate. they proceed only by sensing the others (anonymous) robots.

Collaboration: LIP6

BibTeX

@inproceedings {
	CUT16a,
	title	=	"{Certified Universal Gathering in {\textbackslash}mathbb {R} {\^{}}2 for Oblivious Mobile Robots}",
	author	=	" P. Courtieu and X. Urbain and S. Tixeuil and L. Rieg ",
	booktitle	=	"{DISC 2016, Distributed Computing 30th International Symposium}",
	year	=	2016,
	edition	=	"Springer",
	month	=	"September",
	series	=	"LNCS",
	volume	=	9888,
	pages	=	"187-200",
	address	=	"Paris, France",
	doi	=	"10.1007/978-3-662-53426-7_14",
}