View source for Termination Competition 2025

The Termination and Complexity Competition (termCOMP) 2025 will be affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be shortly before WST, followed by a bug/conflict reporting phase and allowance for bug fixes.
The final run and a presentation of the final results will be live at WST.

<!--
== Results ==
[https://termcomp.github.io/Y2024/ Results]
-->

== Dates  ==

TBA
<!--
* June 19: Benchmark Submission
* June <s>12</s> <s>19</s> 21, 10am CEST: Tool Submission
* June <s>19</s> 24: First Run
* June <s>26</s> 30: Bugfix Deadline
* July 3/4: Final Run
* July 5: Presentation of the results at IJCAR
-->

== Competition Categories ==

The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...)

Proposals for new categories are welcome.

A category is only run at the competition if there are at least 2 participants and at least 40 examples 
for this category in the underlying termination problem data base.

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 seconds. Further technical information is available [[Termination Competition 2025 technical details|here]].
<!--
, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory, and the problem file name is given as the command line argument.
Extra info can be obtained from environment variables, cf. [[Termination Competition 2014 technical 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 [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.

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).

A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.
The SC will decide what should be penalized, depending on the discussion among the participants.

== Steering Committee ==

* Florian Frohn (Chair and Organizer), RWTH Aachen
* Jürgen Giesl, RWTH Aachen 
* Georg Moser, University of Innsbruck
* Étienne Payet, Université de La Réunion
* Akihisa Yamada, AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository] (for rewriting and integer transition systems) or the [https://github.com/TermCOMP/TPDB TPDB repository] (for programming languages).

We recommend to register early, and update information as needed.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== Technical Details ==

Competition data will be presented via [https://github.com/TermCOMP/starexec-master starexec-master]
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).

Technical details about the execution platform are available [[Termination Competition 2025 technical details|here]].

== Contact ==

Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de

To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. 

== Changes with respect to 2024 ==

These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. 
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,
or create a new wiki page and put a link here.

Adopted changes:

* We will use the new ARI format for all Integer Transition System categories, see [https://termination-portal.org/wiki/Term_Rewriting#Integer_Transition_Systems here] for details and [https://github.com/TermCOMP/its-conversion here] for a converter.

Proposed changes:

* We plan to use CPF 3, see [http://cl-informatik.uibk.ac.at/isafor/cpf3.html here] for details and a converter.
* On the RWTH cluster, our computing time is limited. As it's difficult to predict how much testing will be needed on the new platform before the competition, I (Florian) would like to run the competition with a 60 instead of 300s timeout to avoid running out of credits. If things go well, we can switch back to a 300s timeout in 2026.