Termination Competition Certified Categories Competition

See the CPF-website for further details on the certificate format.

The certified categories will be run as follows:

• Tools that can produce output in CPF and that participate in the certified competition are run in parallel to the tools which do not generate CPFs. (Tools may register several times for the same category: uncertified, and CPF-generating w.r.t. certain certifiers.)
• The certifiers are then executed on all generated CPFs.

The more detailed technical description for the certified competition is as follows.

• Termination tools should provide a script which gets as only arguments the name of the file of a TRS and the timeout in seconds.

They should output YES / NO / MAYBE where in the first two cases a proof in CPF 3 has to be printed afterwards. If your tool generates CPF 2 files, then please include the converter from CPF 2 to CPF 3 (available from the CPF-website) into your run scripts. Every output that does not correspond to this format will be refused. (This is done via xmllint example_proof.xml --huge --noout --schema cpf3.xsd)

The platform will ensure that the termination proof for the TRS and the answer correspond to the one in the certificate.

• For complexity tools the workflow is the same, where from the answer YES(*,O(n^i)) / YES(*,O(1)) the polynomial degree i / 0 of the complexity is extracted.