[Termtools] New Format for Certification Termination Competition

[René Thiemann]

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