[Termtools] New Format for Certification Termination Competition

[Frederic Blanqui]

Hello!

For your information, the SVN version of Rainbow now supports:

the following formats for termination problems:
- the old TPDB format http://www.lri.fr/~marche/tpdb/format.html,
- the new TPDB format http://dev.aspsimon.org/xtc.xsd,
- its own format grammar/problem.xsd.

the following formats for termination certificates:
- the new common format http://cl-informatik.uibk.ac.at/software/cpf/,
- its own format grammar/proof.xsd.

See http://color.inria.fr/ for more details.

Best regards, Frederic.


René Thiemann a écrit :
> Dear all,
> 
> we are happy to inform you that all current certifiers (CoLoR/Rainbow,  
> CiME/Coccinelle, CeTA) have agreed to support a common "Certification  
> Problem Format" (CPF). Hence, termination tools just have to output  
> their proofs in the CPF format and can directly use all three  
> certifiers.
> 
> All elements in CPF are documented, there are several examples, and  
> also tools are provided, e.g. there is a pretty-printer from CPF to  
> HTML.
> 
> We currently know that TTT2 and CiME plan to output proofs in CPF. And  
> we would like to encourage also every other termination tool to  
> provide an export to CPF. If you do so, please tell us because then  
> every certification tool can use your tool for tests and benchmarks.  
> Moreover, then perhaps some bug in your tool is detected and can be  
> removed.
> 
> For more details on the format just visit
> 
> http://cl-informatik.uibk.ac.at/software/cpf/
> 
> Best regards,
> the CoLoR / Coccinelle / CeTA - groups
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools