Certified impossibility results and analyses in Coq of some randomised distributed algorithms

Abstract

Randomised algorithms are generally simple to formulate. However,their analysis can become very complex,especially in the field of distributed computing. In this paper,we formally model in Coq a class of randomised distributed algorithms. We develop some tools to help proving impossibility results about classical problems and analysing this class of algorithms. As case studies,we examine the handshake and maximal matching problems. We show how to use our tools to formally prove properties about algorithms solving those problems.