Termination-Portal.org - Recent changes [en]

Termination Competition 2026

Ffrohn — Thu, 09 Jul 2026 09:04:03 GMT

File:Proc WST 2025.pdf

Hofbauer — Mon, 29 Jun 2026 14:56:39 GMT

Hofbauer reverted File:Proc WST 2025.pdf to an old version Reverted to version as of 14:53, 29 June 2026 (UTC)

New page

== Summary ==
Proceedings of WST 2025

File:Proc WST 2025.pdf

Hofbauer — Mon, 29 Jun 2026 14:54:08 GMT

Hofbauer reverted File:Proc WST 2025.pdf to an old version Reverted to version as of 09:20, 13 March 2026 (UTC)

New page

== Summary ==
Proceedings of WST 2025

File:Proc WST 2025.pdf

Hofbauer — Mon, 29 Jun 2026 14:53:05 GMT

Hofbauer uploaded a new version of File:Proc WST 2025.pdf

New page

== Summary ==
Proceedings of WST 2025

Termination Competition 2026

Ffrohn — Fri, 26 Jun 2026 10:01:48 GMT

Termination Competition Certified Categories Competition

Thiemann — Wed, 17 Jun 2026 08:25:36 GMT

updated some parts of the very outdated description of certified category (might require further changes)

Termination Competition 2026

Thiemann — Wed, 17 Jun 2026 08:04:04 GMT

change website of CPF

21st International Workshop on Termination

Ffrohn — Tue, 16 Jun 2026 13:36:06 GMT

File:TermCOMP26 program.png

Ffrohn — Tue, 16 Jun 2026 13:32:34 GMT

Ffrohn uploaded File:TermCOMP26 program.png

New page

@@ Line 93: / Line 93: @@
 * Akihisa Yamada
 * Dieter Hofbauer, ASW Saarland
 == Changes with respect to 2025 ==

@@ Line 20: / Line 20: @@
 * Live Run: July 24/25
 * Presentation of the results at WST: July 25
 == Competition Categories ==
@@ Line 52: / Line 61: @@
 To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].
-Every participant must submit at least five new '''secret''' benchmarks via email to florian.frohn@cs.rwth-aachen.de (unless the size of the benchmarks exceeds 5MB -- in that case, please get in touch to figure out another way).
+Every participant must submit between 5 and 20 new '''secret''' benchmarks via email to florian.frohn@cs.rwth-aachen.de (unless the size of the benchmarks exceeds 5MB -- in that case, please get in touch to figure out another way).
 Please also include a README with a (short) description of the origin of the benchmarks.
 After the competition, these benchmarks will become part of TPDB.
@@ Line 92: / Line 102: @@
 Proposed changes:
-* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.
+* <s>In addition to the usual tracks, we will try to organize a '''knockout tournament'''.</s>
 Adopted changes:
 * We will only run categories with clearly defined rules in the [https://github.com/TermCOMP/termcomp-reference termination competition reference].
-* Every participant has to submit at least five new '''secret''' benchmarks
+* Every participant has to submit at least 5 and at most 20 new '''secret''' benchmarks.
 * Demo categories will only be run on request to the steering committee, and this request has to be justified somehow (e.g., by a paper, significant tool improvements, ...). The final decision is up to the SC.
 * Submissions to TPDB must have a README with a (short) description of the origin of the benchmarks.
 * We will do a full run and a live run, as described above.

@@ Line 1: / Line 1: @@
-Some new elements have been added to the certification problem format.
+See the [https://isafor-ceta.uibk.ac.at/cpf3.html CPF-website] for further details on the certificate format.
@@ Line 9: / Line 5: @@
 * 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 run on all generated CPFs.
+* 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 TRS-file (in XTC-format) and the timeout in seconds.
+* Termination tools should provide a script which gets as only arguments the name of the file of a TRS and the timeout in seconds.
 <blockquote>
-In one-pass mode, it is assumed that there is one script which takes as input a CPF-file and the XTC-file in this order and terminates normally if the proof is accepted, and with some error-code if it is not accepted. If the certifier does not accept, it should start its output with UNSUPPORTED or REJECTED on stdout, to differentiate between both outcomes.
+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)
 </blockquote>
 <blockquote>
-In two-pass mode, there have to be two scripts. The first one takes as input a CPF-file and the XTC-file as before and produces some proof-script on standard-out if everything is fine or exits with some error-code which is interpreted as UNSUPPORTED. The second script is then invoked with the filename of the proof-script and should call the corresponding proof-assistent like Coq, Isabelle, ... It should again exit normally if the proof-script is accepted and with some error-code, otherwise, which is interpreted as REJECTED. Here, both the generated proof-script as well as the output of Coq, Isabelle, ... will be stored.
+The platform will ensure that the termination proof for the TRS and the answer correspond to the one in the certificate.
 </blockquote>
-<blockquote>
+* 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.

@@ Line 42: / Line 42: @@
 Further technical information is available [[Termination Competition 2026 technical details|here]].
-The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.
+The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [https://isafor-ceta.uibk.ac.at/cpf3.html CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.
 For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

@@ Line 71: / Line 71: @@
 as challenges for termination analysis in different categories.
 In 2026, the Termination Competition will run live (in parallel to the FLoC workshops, on the 24th and 25th of July). <!--Tool/benchmark authors are invited to submit a short tool paper and give a presentation on the workshop.-->
 <!--