Termination is an important and difficult problem. Many criteria and tools have been developed over the last years. They are more and more complex and applied on larger and larger systems. For these tools to be used in the certification of critical systems and proof assistants, their results must be certified. Rainbow aims at certifying the termination proofs found by these tools.
Termination provers using Rainbow: AProVE, MatchBox, TPA, TTT2.
Related tools: CiME3 (based on the Coq library Coccinelle) and CeTA (based on the Isabelle/HOL library IsaFoR).
The current version of Rainbow generates a Coq script using the CoLoR library that is then checked by the Coq compiler. See the following slides and this paper for some presentation. More papers are provided in this bibliography. A standalone version based on Coq extraction mechanism is under development.
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.
Last release: 5 November 2010
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 downloading the software. The development version is available on gforge.inria.fr/projects/rainbow/.
Active contributors: Frédéric Blanqui (INRIA, France), Kim-Quyen Ly (INRIA/University Joseph Fourier, Vietnam)
Past contributors: Adam Koprowski (Radboud University, The Netherlands).