[Termtools] Rainbow: new release
Frederic Blanqui
frederic.blanqui at inria.fr
Mon Dec 7 09:43:53 CET 2009
Hello!
On http://color.inria.fr, you will find a new release of Rainbow, an
automated verifier of termination certificates.
Since the last release on March 16, Rainbow can now:
- supports the following termination problem formats: the old TPDB
formats .trs/.srs, the new TPDB format.xtc and its own format .pb.
- supports the following termination certificates formats: the format
.xtc and its own format .prf.
- verify loops for relative (including modulo AC) TRSs or SRSs (in CPF,
use an attribute [type="rel"] for relative or AC steps).
- verify all argument filterings (including collapsing ones, but without
permutation of arguments) both as system transformations or for defining
reduction orderings.
- flat context closure, root labelling and unlabelling.
- verify RPO proofs by using the Coccinelle library
(http://a3pat.ensiie.fr/).
Finally, Rainbow efficiency in Coq has been improved. Some recent
experiments show that Rainbow can verify more than 700 certificates
obtained from TRS problems (instead of 558 in last year competition),
each certificate being verified in about 6s in average (0.5s for loops),
that is about 25% of the time required for finding the certificate.
Feedbacks on using Rainbow are very welcome!
More information about the Termtools
mailing list