[Termtools] New Format for Certification Termination Competition

[Carsten Fuhs]

Dear René,

that's great news! Having standard data formats like CPF to make 
interoperability convenient is definitely a good thing. Indeed, for
the next competition, AProVE also plans to output proofs in CPF.

Best regards,

  Carsten

On Wednesday 26 August 2009 11:14, René Thiemann wrote:
> 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



-- 
Carsten Fuhs          mailto:fuhs at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/fuhs
RWTH Aachen           phone: +49 241 80-21241