Dear all, termCOMP '25 will take place during WST '25 (3./4.9.). As StarExec will be discontinued in June, quite a few things will change. Hence, I'd like to give you a heads up. First, note that the results of previous competitions (even those from pre-StarExec times) have been archived [1]. In 2025, the competition will take place on the RWTH Aachen HPC cluster. The infrastructure for running the competition and displaying results is mostly ready (e.g., you can see the results of a test run that I've done today here [2]). We can use Docker, so it should be rather easy to participate. Currently, the intended workflow is as follows: 1. Build a docker image with your tool. During the competition, the following commands will be invoked within the docker container: * solver --name * solver --timeout=$timeout --category=$category $benchmark So an executable named "solver" must be available in your container. The former command must print the name of your solver to stdout. The latter is (hopefully) self-explaining. I'll provide a list with the exact category names at some point, but they will essentially be identical to the names of the corresponding TPDB directories. 2. Upload your docker image to docker hub [3]. 3. Register your tool by providing the identifier of your image on docker hub, and the categories where you want to participate. Presumably, we will again use a GitHub repository and pull requests to do that semi-automatically. Please let me know if the procedure outlined above doesn't work for you (and why). One major drawback of the new setup is that participants cannot test by themselves. Once the technical details are fixed, I can start running test jobs, but I won't be able to test all solvers shortly before the competition. Hence, if you want your solver to be tested before the first run, register as early as possible. Further "minor" changes compared to last year (also detailed here [4]): * We will use the new ARI format for all Integer Transition System categories, see [5] for details and [6] for a converter. * We plan to use CPF 3, see here [7] 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 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. Please let me know if you have any questions / remarks / suggestions. Moreover, if somebody wants to propose a new category, please do so as early as possible, so that we have time to discuss the details. Best Florian [1] https://termcomp.github.io/ [2] https://termcomp.verify.rwth-aachen.de/Y2025/ [3] https://hub.docker.com/ [4] https://termination-portal.org/wiki/Termination_Competition_2025#Changes_wit... [5] https://termination-portal.org/wiki/Term_Rewriting#Integer_Transition_System... [6] https://github.com/TermCOMP/its-conversion [7] http://cl-informatik.uibk.ac.at/isafor/cpf3.html