We consider the problem of gathering in finite time and at the same location, not known beforehand, a set of deterministic semi-synchronous robots, starting from an arbitrary initial configuration that may even be bivalent (that is, a configuration where the robots are evenly split on two different locations). This problem is known to be unsolvable when the robots are oblivious, that is, when they cannot remember their past actions. We present two deterministic gathering algorithms where robots may remember and communicate a single bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solutions are thus memory optimal and self-stabilizing. The first algorithm makes use of multiplicity detection, while the second solely uses robot colors. Their proof of correctness is formally certified by the Coq proof assistant using the Pactole framework.

International audience

We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.

Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensured.This paper presents the approach developed in Project A3PAT to discover and moreover certify, with full automation, termination proofs for term rewriting systems.