CoLoR project: Certification of termination proofs

TCG | Rainbow | CoLoR | Bibliography | Competition

Goal: Termination is an important and difficult problem. Many criteria and tools have been developed over the last years. See for instance the annual international termination competition. 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. This project aims at certifying the termination proofs found by these tools by providing:

• TCG: a grammar for termination certificates
• CoLoR: a Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems
• Rainbow: a program automatically generating Coq proofs from the termination certificate grammar and the CoLoR library

See the following slides and this paper for some presentation. More papers are provided in the following bibliography.

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.

Termination provers using Rainbow: AProVE, MatchBox, TPA, TTT2

Other developments using CoLoR: Spi [tar.gz], ABTR, ProofOS

Results of the termination competitions

News:

• 10-12-13: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. F. Blanqui and A. Koprowski. To appear in MSCS.
• 10-10-28: new release of CoLoR compiling with Coq 8.3.
• 10-02-24: results of 2009 termination competition (Rainbow is 2nd).
• 09-12-07: new releases of CoLoR and Rainbow.
• 09-06-03: Automated Verification of Termination Certificates, F. Blanqui and A. Koprowski, INRIA Research Report 6949.
• 08-11-14: Rainbow+CoLoR is the best certification back-end for termination proofs for two consecutive years. See the results.
• 07-06-07: TPA+Rainbow+CoLoR won the 2007 certified termination competition. See the results.

Events:

• 10-07-16: 7th International Competition of Termination Provers, Edinburgh, UK
• 10-07-14: 11th International Workshop on Termination (WST 2010), Edinburgh, UK
• 10-07-11: 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Edinburgh, UK
• 09-06-03: 10th International Workshop on Termination (WST'09), Leipzig, Germany
• 08-05-17: Workshop on Certified Termination (WScT'08), 17-19 May 2008, Leipzig
• 07-07-12: Johannes Waldmann's report on the 2007 termination competition
• 07-05-11: 1st Workshop on the certification of termination proofs

• the new TPDB format XTC
• the old TPDB format
• its own format problem.xsd

Rainbow supports two formats for termination certificates:

• CPF
• its own format proof.xsd

News:

• 09-08-26: CPF: new format for termination certificates

News: CHANGES

• 10-11-05: new release compatible with OCaml 3.12, Coq 8.3 and CoLoR 101102
• 09-12-07: new release
• 09-09-04: added support for the XTC and CPF formats
• 09-07-17: flat context closure, root labelling and unlabelling
• 09-05-22: certification of loops
• 09-04-09: migration from CVS to SVN
• 09-03-16: new release
• 09-02-10: XML-Light and TPDB tools are now included in Rainbow
• 08-11-10: unification-based graph decomposition
• 08-11-10: rewriting modulo regular theories (e.g. C/AC)
• 07-07-13: new release
• 07-05-25: relative termination problems
• 07-05-24: argument filtering
• 07-05-18: dependency pairs transformation
• 07-04-25: matrix interpretations
• 06-10-24: name space problems fixed
• 06-07-21: polynomial interpretations

TPDB termination problems supported by Rainbow: [TPDB]

• TRS standard
• TRS relative
• TRS modulo equations l=r with Var(l)=Var(r) (e.g. associativity and commutativity) are translated into TRS relative
• SRS standard
• SRS relative

Proof techniques supported by Rainbow:

• unlabelling
• root labelling
• flat context closure
• dependency pair transformation (with or without marked symbols)
• dependency graph decomposition (with unification)
• polynomial interpretation
• matrix interpretation (standard, arctic and below-zero)
• argument filtering
• reversal (for SRSs or unary TRSs)

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)

Past contributors: Adam Koprowski (Radboud University, The Netherlands).

See this paper for some presentation. More papers are provided in the bibliography below.

News: CHANGES

• 10-10-28: new release compiling with Coq 8.3
• 09-12-07: new release
• 09-11-04: added Dershowitz's improvement for computing dependency pairs
• 09-11-02: variable condition violation
• 09-10-30: added conversion from CoLoR terms to Coccinelle terms
• 09-07-08: flat context closure, root labelling
• 09-06-26: semantic labelling
• 09-06-19: arguments filterings with projections
• 09-05-22: non-termination of loops
• 09-04-09: migration from CVS to SVN
• 09-03-11: new release compiling with Coq 8.2
• 08-10-31: unification-based dependency graph approximation
• 08-10-31: syntactic unification
• 08-08-08: dependency graph decomposition
• 08-05-09: new release compiling with Coq 8.1pl3
• 08-03-14: arctic interpretations
• 07-08-23: strongly connected components
• 07-08-06: support for classical reasoning
• 07-07-13: new release
• 07-05-25: conversion from strings to algebraic terms
• 07-04-25: semi-rings and matrix interpretations
• 07-03-22: new release compiling with Coq 8.1
• 07-02-09: termination based on dependency graph cycles
• 06-12-01: total completion of a relation
• 06-12-01: modularity of (relative) termination

Content: BROWSE DEFINITIONS AND THEOREMS

• (Non-)Termination criteria:
  • loops
  • polynomial interpretations
  • matrix interpretations (standard, arctic and below-zero)
  • first and higher order recursive path ordering
  • lexicographic and multiset ordering
• Transformation techniques:
  • flat context closure
  • semantic labelling
  • dependency graph decomposition based on unification
  • dependancy pairs transformation
  • arguments filtering
  • reversal of SRSs or unary TRSs
  • conversions strings -> algebraic terms -> varyadic terms
• Term structures:
  • strings
  • algebraic terms with symbols of fixed arity
  • varyadic terms
  • simply typed lambda-terms
• Data structures:
  • matrices
  • finite multisets
  • polynomials with multiple variables
  • vectors/arrays
• Mathematical structures:
  • (ordered) semi-rings
  • relations/graphs

Download: This library 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/color/.

Active contributors: Frédéric Blanqui (INRIA, France), Sidi Ould-Biha (INRIA, France), Kim-Quyen Ly (INRIA internship, Viet-Nam), Adam Koprowski (Radbound University, The Netherlands), Johannes Waldmann (Leipzig HTWK, Germany)

Past contributors: Sorin Stratulat (Université Paul Verlaine, Metz, France), Julien Bureaux (ENS Paris, France), Pierre-Yves Strub (INRIA, France), Wang Qian (Tsinghua University, China), Zhang Liany (Tsinghua University, China), Hans Zantema (Radboud University, Nijmegen, The Netherlands), Jörg Endrullis (Amsterdam Vrije Universiteit, The Netherlands), Stéphane Le Roux (ENS Lyon, France), Léo Ducas (ENS Paris, France), Solange Coupet-Grimal (Université de Provence Aix-Marseille I, France), William Delobel (Université de Provence Aix-Marseille I, France), Sébastien Hinderer (LORIA, France)

• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. F. Blanqui and A. Koprowski, to appear in MSCS, 2011.
• Coq formalization of the higher-order recursive path ordering, A. Koprowski, Applicable Algebra in Engineering Communication and Computing 20(5-6):379-425, 2009.
• Automated Verification of Termination Certificates, F. Blanqui and A. Koprowski, INRIA Research Report 6949, 2009.
• Automated Verification of Termination Certificates, F. Blanqui, Talk at East China Normal University, Shanghai, 3 December 2008.
• Termination of rewriting and its certification, A. Koprowski, PhD Thesis, 2008.
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations, A. Koprowski and H. Zantema, SOFSEM'08.
• Arctic termination... below zero, A. Koprowski and J. Waldmann, RTA'08.
• Acyclicity and Linear Extendability: a Formal and Constructive Equivalence, S. Le Roux, TPHOL'07.
• Certification of Matrix Interpretations in Coq, A. Koprowski and H. Zantema, WST'07.
• Automated Certification of Termination Proofs, F. Blanqui, Invited talk, TYPES'07.
• CoLoR, a Coq Library on Rewriting and termination, F. Blanqui, S. Coupet-Grimal, W. Delobel, S. Hinderer and A. Koprowski, WST'06. [slides]
• A Formalization of the Simply Typed Lambda Calculus in Coq, A. Koprowski, Manuscript, 2006.
• A Constructive Axiomatization of the Recursive Path Ordering, S. Coupet-Grimal and W. Delobel, Research report 28, LIF, Université de la Méditerranée, 2006.
• An Effective Proof of the Well-Foundedness of the Multiset Path Ordering, S. Coupet-Grimal and W. Delobel, Applicable Algebra in Engineering Communication and Computing 17(6):453-469, 2006.
• Certified Higher-Order Recursive Path Ordering, A. Koprowski, RTA'06.
• An Effective Proof of the Well-Foundedness of the Multiset Path Ordering, S. Coupet-Grimal and W. Delobel, JFLA'06.
• Well-foundedness of the Higher-Order Recursive Path Ordering in Coq, A. Koprowski, Master thesis, 2004.
• Certification des preuves de termination par interprétations polynomiales, S. Hinderer, Master thesis, 2004.
• Well-foundedness of the Recursive Path Ordering in Coq, N. de Kleijn, A. Koprowski and F. van Raamsdonk, Dutch Proof Tools Day, 2004.
• Well-foundedness of RPO in Coq, N. de Kleijn, Master thesis, 2003.

A3PAT:

• A3PAT, an Approach for Certified Automated Termination Proofs, E. Contejean, P. Courtieu, O. Pons, X. Urbain, J. Forest and A. Paskevich, PEPM'10.
• Certifying a Termination Criterion Based on Graphs, without Graphs, P. Courtieu, J. Forest and X. Urbain, TPHOL'08
• Deep-Embedded Unification, E. Contejean, J. Forest and X. Urbain, CEDRIC Research Report 1547, 2008.
• Certification of automated termination proofs, E. Contejean, P. Courtieu, J. Forest, O. Pons and X. Urbain, FroCos'07.
• Modelling permutations in Coq for Coccinelle, E. Contejean, Essay Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, LNCS 4600, 2007.
• Certification des preuves de terminaison en Coq, T. Hubert, Master thesis, 2004.
• A certified AC matching algorithm, E. Contejean, RTA'04.

CeTA:

• Certified Subterm Cirterion and Certified Usable Rules, C. Sternagel and R. Thiemann, RTA'10.
• CeTA - A Tool for Certified Termination Analysis, C. Sternagel, R. Thiemann, S. Winkler and H. Zankl, WST'09.
• Finding and Certifying Loops, H. Zankl, C. Sternagel, D. Hofbauer and A. Middeldorp, SOFSEM'10.
• Certification of Termination Proofs using CeTA, R. Thiemann and C. Sternagel, TPHOL'09.

Last updated on 4 May 2012. Come back to main page.