Rainbow is a tool for verifying the correctness of CPF termination certificates.
It is itself partly certified in and extracted from Coq, using the CoLoR library. It can also generates Coq scripts.
See the following slides and this paper for some presentation. More papers are provided in this bibliography.
Similar tools are CiME3 (based on the Coq library Coccinelle) and CeTA (based on the Isabelle/HOL library IsaFoR).
Contributions are welcome !
Mailing list: For announcements and discussions about this project, create an account on https://sympa.inria.fr/, log in and subscribe to color.
Rainbow supports the following formats for termination problems:
Rainbow supports two following formats for termination certificates:
Rainbow supports the following termination problems:
Rainbow supports the following termination certificates:
Download: This software is distributed under the terms of the French free software license CeCILL, that is compatible with the GNU General Public License. Read the conditions of the license before getting it on here.
Maintainer: Frédéric Blanqui (INRIA, France)
Contributors: Kim-Quyen Ly (INRIA/University Joseph Fourier, Vietnam), Adam Koprowski (Radboud University, The Netherlands), Frédéric Blanqui (INRIA, France).