Automated Certified Proofs with CiME3

ÉVelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons & Xavier Urbain
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...