Termination-Portal.org - User contributions [en]

21st International Workshop on Termination

2026-02-23T09:23:53Z

Ffrohn: /* Program Committee */

July 25, 2026, Lisbon, Portugal.

As part of [https://www.floc26.org FLoC 2026] and
co-located with [https://www.floc26.org/ijcar IJCAR 2026].

==Background==

The Workshop on Termination (WST) traditionally brings together, in an
informal setting, researchers interested in all aspects of termination,
whether this interest be practical or theoretical, primary or derived.
The workshop also provides a ground for cross-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 21st International Workshop on Termination (WST 2026) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]),
Haifa ([https://sws.cs.ru.nl/WST2022 2022]),
Obergurgl ([https://termination-portal.org/wiki/19th_International_Workshop_on_Termination 2023]), and
Leipzig ([https://www.imn.htwk-leipzig.de/WST2025/ 2025]).

==Workshop Topics==

The 21st International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
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). 



==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://submissions.floc26.org/wst/ the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: 28th of April
* paper submission: 5th of May
* notification: 26th of May
* early registration deadline: 1st of June
* final version: 26th of June
* workshop: 25th of July

==Program Committee==

* Florian Frohn, RWTH Aachen University (co-chair)
* Raúl Gutiérrez, Universitat Politècnica de València
* Dieter Hofbauer, ASW Saarland
* Nils Lommen, RWTH Aachen University
* Johannes Niederhauser, University of Innsbruck
* Vincent van Oostrom, University of Sussex
* Étienne Payet, Université de La Réunion (co-chair)
* Hiroshi Unno, Tohoku University
* Wim Vanhoof, Université de Namur
* Dragana Milovancevic, Imperial College London

Termination Portal

2026-02-23T09:13:18Z

Ffrohn: /* Recent News */

Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).

This portal aims to provide the research community with up-to-date information about the field
of termination analysis.
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),
[[:Category:News|News]] (information about events and new publications),
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and
[[:Category:Bibtex|References]] (publications related to termination analysis).
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].

Have [[Suggestions]] to improve this web resource?
- How to [[Contribute]].

=Recent News=
* [[Termination Competition 2026]]
* [[21st International Workshop on Termination]]
* [[20th International Workshop on Termination]]
* [[Termination Competition 2025]]
* [[Termination Competition 2024]]
* [[Termination Competition 2023]]
* [[19th International Workshop on Termination]]
* [[Termination Competition 2022]]
<DynamicPageList>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</DynamicPageList>
Older news entries can be found on the [[:Category:News|news page]].

Termination Competition 2026

2026-02-23T08:39:34Z

Ffrohn:

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
Test runs will take place right after the submission deadline, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the full run.
A live run on a subset of the benchmark collection, and a presentation of the final results will take place at WST.
Presumably, there will also be a presentation at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* Full Run: July 13-17
* Live Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

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

There will be a full run on the entire benchmark collection '''before''' WST, and a live run on a subset of the benchmark collection at WST.
The timeout for the full run will be 300 seconds.
The timeout for the live run will be significantly smaller (presumably 30 seconds).
The results of the full run will be announced at WST.

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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-18T10:15:10Z

Ffrohn: /* Dates */

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* Full Run: July 13-17
* Live Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

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

There will be a full run on the entire benchmark collection '''before''' WST, and a live run on a subset of the benchmark collection at WST.
The timeout for the full run will be 300 seconds.
The timeout for the live run will be significantly smaller (presumably 30 seconds).
The results of the full run will be announced at WST.

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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-18T10:09:43Z

Ffrohn: /* Changes with respect to 2025 */

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* First Run: July 9/10
* Final Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

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

There will be a full run on the entire benchmark collection '''before''' WST, and a live run on a subset of the benchmark collection at WST.
The timeout for the full run will be 300 seconds.
The timeout for the live run will be significantly smaller (presumably 30 seconds).
The results of the full run will be announced at WST.

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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-18T10:08:49Z

Ffrohn: /* Competition Procedure */

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* First Run: July 9/10
* Final Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

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

There will be a full run on the entire benchmark collection '''before''' WST, and a live run on a subset of the benchmark collection at WST.
The timeout for the full run will be 300 seconds.
The timeout for the live run will be significantly smaller (presumably 30 seconds).
The results of the full run will be announced at WST.

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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.
* Instead of using a fixed timeout as in previous years, the timeout will be determined as described above

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-11T15:42:19Z

Ffrohn: /* Changes with respect to 2025 */

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* First Run: July 9/10
* Final Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

== 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 for each benchmark is determined as follows:
* The minimal timeout is 5 seconds
* The maximal timeout is 300 seconds
* For benchmarks that have not been solved in 2025, the timeout is 300 seconds
* For benchmarks that have been solved in 2025, the timeout is determined by multiplying the runtime of the fastest successful solver by 2, i.e., the runtime is <pre>min(300, max(5, 2 x runtime of last year's fastest solver))</pre>
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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.
* Instead of using a fixed timeout as in previous years, the timeout will be determined as described above

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-11T08:40:22Z

Ffrohn:

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also at IJCAR.



== Dates ==

* Tool and Benchmark Submission: June 26
* First Run: July 9/10
* Final Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

== 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 for each benchmark is determined as follows:
* The minimal timeout is 5 seconds
* The maximal timeout is 300 seconds
* For benchmarks that have not been solved in 2025, the timeout is 300 seconds
* For benchmarks that have been solved in 2025, the timeout is determined by multiplying the runtime of the fastest successful solver by 2, i.e., the runtime is <pre>min(300, max(5, 2 x runtime of last year's fastest solver))</pre>
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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Instead of using a fixed timeout as in previous years, the timeout will be determined as described above
* Demo categories will only be run on request, 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.

Termination Competition 2026

2026-02-11T08:22:19Z

Ffrohn: Created page with "The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], w..."

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be two weeks before WST, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the final run.
The final run and a presentation of the final results will be live at WST, and presumably also either at IJCAR, or in the context of the FLoC Olympics..



== Dates ==

* Tool and Benchmark Submission: June 26
* First Run: July 9/10
* Final Run: July 24/25
* Presentation of the results at WST: July 25

== 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, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules.

== 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 for each benchmark is determined as follows:
* The minimal timeout is 5 seconds
* The maximal timeout is 300 seconds
* For benchmarks that have not been solved in 2025, the timeout is 300 seconds
* For benchmarks that have been solved in 2025, the timeout is determined by multiplying the runtime of the fastest successful solver by 2, i.e., the runtime is <pre>min(300, max(5, 2 x runtime of last year's fastest solver))</pre>
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.

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
* Dieter Hofbauer, ASW Saarland

== Registration ==

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

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

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

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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).



== 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 2025 ==

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.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules.
* Every participant has to submit at least five new '''secret''' benchmarks
* Instead of using a fixed timeout as in previous years, the timeout will be determined as described above
* Demo categories will only be run on request, 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.

21st International Workshop on Termination

2026-01-19T13:20:40Z

Ffrohn: /* Important Dates */

July 25, 2026, Lisbon, Portugal.

As part of [https://www.floc26.org FLoC 2026] and
co-located with [https://www.floc26.org/ijcar IJCAR 2026].

==Background==

The Workshop on Termination (WST) traditionally brings together, in an
informal setting, researchers interested in all aspects of termination,
whether this interest be practical or theoretical, primary or derived.
The workshop also provides a ground for cross-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 21st International Workshop on Termination (WST 2026) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]),
Haifa ([https://sws.cs.ru.nl/WST2022 2022]),
Obergurgl ([https://termination-portal.org/wiki/19th_International_Workshop_on_Termination 2023]), and
Leipzig ([https://www.imn.htwk-leipzig.de/WST2025/ 2025]).

==Workshop Topics==

The 21st International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
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). 



==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://submissions.floc26.org/wst/ the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: 28th of April
* paper submission: 5th of May
* notification: 26th of May
* early registration deadline: 1st of June
* final version: 26th of June
* workshop: 25th of July

==Program Committee==

TBA

WST

2026-01-15T15:00:40Z

Ffrohn:

The International Workshop on Termination (WST) brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [[21st International Workshop on Termination]] during [https://www.floc26.org/ Federated Logic Conference (FLoC)], Lisbon, Portugal, July 25, 2026.

Previous workshops:
* [https://www.imn.htwk-leipzig.de/WST2025/ 20th International Workshop on Termination], Leipzig, Germany, September 3-4, 2025. ([https://termcomp.imn.htwk-leipzig.de/WST2025/ alternative web server])
* [[19th International Workshop on Termination]], Obergurgl, Austria, August 24-25, 2023.
* [https://sws.cs.ru.nl/WST2022 18th International Workshop on Termination] during [https://www.floc2022.org/ Federated Logic Conference (FLoC)], Haifa, Israel, August 11-12, 2022.
* [http://costa.fdi.ucm.es/wst2020/ 17th International Workshop on Termination] planned to be co-located with IJCAR and [http://fscdconference.org/editions/upcoming FSCD 2020], Paris (France), June/July, 2020.
* [https://web.archive.org/web/20181026074549/http://wst2018.webs.upv.es/ 16th International Workshop on Termination] during [http://www.floc2018.org/ Federated Logic Conference (FLoC)], Oxford, United Kingdom, July 18-19, 2018.
* [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] at [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps], Obergurgl, Austria, September 5-7, 2016.
* [https://easychair.org/smart-program/VSL2014/WST-index.html 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014.
* Joint Workshop on Termination [https://web.archive.org/web/20140505184545/https://www.imn.htwk-leipzig.de/WST2013/ WST2013] and on Foundational and Practical Aspects of Resource Analysis [http://fopara2013.cs.unibo.it/ FOPARA], Bertinoro, Italy, August 29-31, 2013.
* [https://web.archive.org/web/20120704083358/http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 12th International Workshop on Termination, Obergurgl, February 19-23, 2012].
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010].
* [https://web.archive.org/web/20160910020839/https://portal.imn.htwk-leipzig.de/termine/10-international-workshop-on-termination/ 10th International Workshop on Termination, Leipzig, 2009].
* [https://web.archive.org/web/20181130121956/http://www.lsv.fr/Events/rdp07/wst.html International Workshop on Termination, Paris, 2007].
* [https://web.archive.org/web/20060620011616/http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Termination, Seattle, 2006].
* [https://web.archive.org/web/20050503110144/http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Termination, Aachen, 2004].
* [https://web.archive.org/web/20090413162845/http://users.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Termination, Valencia, 2003].
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Termination, Utrecht, 2001].
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Termination, Dagstuhl, 1999].
* [https://web.archive.org/web/20030829111237/http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997].
* [https://lics.siglog.org/newsletters/22.html 2nd International Workshop on Termination, La Bresse, 1995].
* 1st International Workshop on Termination, St. Andrews, 1993.

Independently from WST, there are meetings on Certified Termination : [[WScT]]

WST

2026-01-15T15:00:20Z

Ffrohn:

The International Workshop on Termination (WST) brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [[21st International Workshop on Termination]] during [https://www.floc2026.org/ Federated Logic Conference (FLoC)], Lisbon, Portugal, July 25, 2026.

Previous workshops:
* [https://www.imn.htwk-leipzig.de/WST2025/ 20th International Workshop on Termination], Leipzig, Germany, September 3-4, 2025. ([https://termcomp.imn.htwk-leipzig.de/WST2025/ alternative web server])
* [[19th International Workshop on Termination]], Obergurgl, Austria, August 24-25, 2023.
* [https://sws.cs.ru.nl/WST2022 18th International Workshop on Termination] during [https://www.floc2022.org/ Federated Logic Conference (FLoC)], Haifa, Israel, August 11-12, 2022.
* [http://costa.fdi.ucm.es/wst2020/ 17th International Workshop on Termination] planned to be co-located with IJCAR and [http://fscdconference.org/editions/upcoming FSCD 2020], Paris (France), June/July, 2020.
* [https://web.archive.org/web/20181026074549/http://wst2018.webs.upv.es/ 16th International Workshop on Termination] during [http://www.floc2018.org/ Federated Logic Conference (FLoC)], Oxford, United Kingdom, July 18-19, 2018.
* [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] at [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps], Obergurgl, Austria, September 5-7, 2016.
* [https://easychair.org/smart-program/VSL2014/WST-index.html 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014.
* Joint Workshop on Termination [https://web.archive.org/web/20140505184545/https://www.imn.htwk-leipzig.de/WST2013/ WST2013] and on Foundational and Practical Aspects of Resource Analysis [http://fopara2013.cs.unibo.it/ FOPARA], Bertinoro, Italy, August 29-31, 2013.
* [https://web.archive.org/web/20120704083358/http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 12th International Workshop on Termination, Obergurgl, February 19-23, 2012].
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010].
* [https://web.archive.org/web/20160910020839/https://portal.imn.htwk-leipzig.de/termine/10-international-workshop-on-termination/ 10th International Workshop on Termination, Leipzig, 2009].
* [https://web.archive.org/web/20181130121956/http://www.lsv.fr/Events/rdp07/wst.html International Workshop on Termination, Paris, 2007].
* [https://web.archive.org/web/20060620011616/http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Termination, Seattle, 2006].
* [https://web.archive.org/web/20050503110144/http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Termination, Aachen, 2004].
* [https://web.archive.org/web/20090413162845/http://users.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Termination, Valencia, 2003].
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Termination, Utrecht, 2001].
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Termination, Dagstuhl, 1999].
* [https://web.archive.org/web/20030829111237/http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997].
* [https://lics.siglog.org/newsletters/22.html 2nd International Workshop on Termination, La Bresse, 1995].
* 1st International Workshop on Termination, St. Andrews, 1993.

Independently from WST, there are meetings on Certified Termination : [[WScT]]

WST

2026-01-15T14:59:18Z

Ffrohn:

The International Workshop on Termination (WST) brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [[21st International Workshop on Termination]], Lisbon, Portugal, July 25, 2026.

Previous workshops:
* [https://www.imn.htwk-leipzig.de/WST2025/ 20th International Workshop on Termination], Leipzig, Germany, September 3-4, 2025. ([https://termcomp.imn.htwk-leipzig.de/WST2025/ alternative web server])
* [[19th International Workshop on Termination]], Obergurgl, Austria, August 24-25, 2023.
* [https://sws.cs.ru.nl/WST2022 18th International Workshop on Termination] during [https://www.floc2022.org/ Federated Logic Conference (FLoC)], Haifa, Israel, August 11-12, 2022.
* [http://costa.fdi.ucm.es/wst2020/ 17th International Workshop on Termination] planned to be co-located with IJCAR and [http://fscdconference.org/editions/upcoming FSCD 2020], Paris (France), June/July, 2020.
* [https://web.archive.org/web/20181026074549/http://wst2018.webs.upv.es/ 16th International Workshop on Termination] during [http://www.floc2018.org/ Federated Logic Conference (FLoC)], Oxford, United Kingdom, July 18-19, 2018.
* [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] at [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps], Obergurgl, Austria, September 5-7, 2016.
* [https://easychair.org/smart-program/VSL2014/WST-index.html 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014.
* Joint Workshop on Termination [https://web.archive.org/web/20140505184545/https://www.imn.htwk-leipzig.de/WST2013/ WST2013] and on Foundational and Practical Aspects of Resource Analysis [http://fopara2013.cs.unibo.it/ FOPARA], Bertinoro, Italy, August 29-31, 2013.
* [https://web.archive.org/web/20120704083358/http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 12th International Workshop on Termination, Obergurgl, February 19-23, 2012].
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010].
* [https://web.archive.org/web/20160910020839/https://portal.imn.htwk-leipzig.de/termine/10-international-workshop-on-termination/ 10th International Workshop on Termination, Leipzig, 2009].
* [https://web.archive.org/web/20181130121956/http://www.lsv.fr/Events/rdp07/wst.html International Workshop on Termination, Paris, 2007].
* [https://web.archive.org/web/20060620011616/http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Termination, Seattle, 2006].
* [https://web.archive.org/web/20050503110144/http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Termination, Aachen, 2004].
* [https://web.archive.org/web/20090413162845/http://users.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Termination, Valencia, 2003].
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Termination, Utrecht, 2001].
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Termination, Dagstuhl, 1999].
* [https://web.archive.org/web/20030829111237/http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997].
* [https://lics.siglog.org/newsletters/22.html 2nd International Workshop on Termination, La Bresse, 1995].
* 1st International Workshop on Termination, St. Andrews, 1993.

Independently from WST, there are meetings on Certified Termination : [[WScT]]

Termination Portal

2026-01-15T14:58:21Z

Ffrohn: /* Recent News */

Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).

This portal aims to provide the research community with up-to-date information about the field
of termination analysis.
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),
[[:Category:News|News]] (information about events and new publications),
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and
[[:Category:Bibtex|References]] (publications related to termination analysis).
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].

Have [[Suggestions]] to improve this web resource?
- How to [[Contribute]].

=Recent News=
* [[21st International Workshop on Termination]]
* [[20th International Workshop on Termination]]
* [[Termination Competition 2025]]
* [[Termination Competition 2024]]
* [[Termination Competition 2023]]
* [[19th International Workshop on Termination]]
* [[Termination Competition 2022]]
<DynamicPageList>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</DynamicPageList>
Older news entries can be found on the [[:Category:News|news page]].

21st International Workshop on Termination

2026-01-15T14:57:58Z

Ffrohn: Created page with "July 25, 2026, Lisbon, Portugal. As part of [https://www.floc26.org FLoC 2026] and co-located with [https://www.floc26.org/ijcar IJCAR 2026]. ==Background== The Workshop..."

July 25, 2026, Lisbon, Portugal.

As part of [https://www.floc26.org FLoC 2026] and
co-located with [https://www.floc26.org/ijcar IJCAR 2026].

==Background==

The Workshop on Termination (WST) traditionally brings together, in an
informal setting, researchers interested in all aspects of termination,
whether this interest be practical or theoretical, primary or derived.
The workshop also provides a ground for cross-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 21st International Workshop on Termination (WST 2026) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]),
Haifa ([https://sws.cs.ru.nl/WST2022 2022]),
Obergurgl ([https://termination-portal.org/wiki/19th_International_Workshop_on_Termination 2023]), and
Leipzig ([https://www.imn.htwk-leipzig.de/WST2025/ 2025]).

==Workshop Topics==

The 21st International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
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). 



==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://submissions.floc26.org/wst/ the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

TBA



==Program Committee==

TBA

TPDB

2025-10-31T10:51:57Z

Ffrohn: /* Data */

The Termination Problems Data Base collects termination problems
that are being used in termination competitions.

== Syntax and semantics specification ==

* for versions from 11.* onwards (XML format): [https://github.com/TermCOMP/TPDB/raw/master/xml/xtc.xsd xtc.xsd], already part of the [https://github.com/TermCOMP/TPDB TPDB]
* for versions from 7.* onwards (XML format): [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd xtc.xsd], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB]
* for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html

see also:

* output specification for certified categories: http://cl-informatik.uibk.ac.at/software/cpf/

== Data ==
* since 2024: https://github.com/TermCOMP/TPDB-ARI
* version 11.0 (2019): https://github.com/TermCOMP/TPDB
* version 9.0 (2014), 10.3 (2015), 10.4 (2016), 10.5 (2017), 10.6 (2018) http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2012) and 8.0.7 (2013) http://termcomp.uibk.ac.at/status/downloads/
* version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz
* version 5.0.2 (2008..2009) http://termcomp.uibk.ac.at/termcomp/docs/tpdb-5.0.2.tar.gz
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/

== Sources ==

TPDB problems are collected from a variety of sources, by a variety of contributors. Often, the author of the problem is not the creator of the respective TPDB file. Sometimes, TPDB file structure (directory names) have been changed.

The following are references for classical problem sets that appear in TPDB.

* TRS/SK90 Joachim Steinbach, Ulrich Kühler: Check your Ordering - termination proofs and open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990.
* TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf
* TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps
* SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?). They include (as z027 .. z064) a set of one-rule termination problems by Alfons Geser (Habilitationsschrift, Tübingen, 2001) and possibly Winfried Kurth (Dissertation, Clausthal, 1990)

And here are some extra bits of trivia.

* SRS termination problems ICFP_2010 and ICFP_2010_relative were produced by participants of the ICFP 2010 programming contest, organized by Bertram Felgenhauer and Johannes Waldmann. ''All'' of these problems are terminating by construction. See https://www.imn.htwk-leipzig.de/~waldmann/talk/10/icfp/

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://cl-informatik.uibk.ac.at/users/thiemann/convert.jar, usage:

java -jar convert.jar someTrs.trs > someTrs.xml

* converter from 7.* (XML) format to pre-7 (textual) format: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB], usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

* converter from 7.* (XML) format to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl], see explanation at http://lists.lri.fr/pipermail/termtools/2018-July/001212.html

* Haskell library for reading and writing TPDB (plain and XML format) [http://hackage.haskell.org/package/tpdb]

Termination Competition 2025 technical details

2025-10-02T07:14:24Z

Ffrohn: /* Execution Environment */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t. the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.
* If your solver needs to write to temporary files, write them to <code>/tmp</code>. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

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

== Certification ==

We use CeTA version 3.6 for certification.

Termination Competition Steering Committee

2025-09-18T09:36:32Z

Ffrohn:

The basic ideas are:
* one research group hosts (implements, executes) the competition
* a committee, representing all research groups, influences the design and the running of the competition.

Currently, the Competition is hosted on StarExec.

The Competition Committee currently
consists of
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

[[Termination_Competition_Steering_Committee_Bylaws]]

The steering committee assembled on June 3rd, 2009,
during the Workshop on Termination in Leipzig.

[[TC_SC_Meeting_WST09]]

= Current Votes =

= Proposed Votes =

The Competition Committee should vote on ...
(give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)

= Earlier Votes / Issues resolved otherwise =

(otherwise = These topics were discussed on the mailing list,
some solution emerged and no-one objected.)

* (asked 31-Oct-2008) what is the timeout that will be applied
for verification (by coqc) of the termination certificates:

<poll>
Timemout for verification
1 minute
3 minutes
10 minutes
</poll>

deadline for voting: Monday 3-Nov 12:00 noon CET.

See discussion at http://lists.lri.fr/pipermail/termtools/2008-October/000594.html

Resolution: 1 minute timeout.

* When should the competition start? (asked 30-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000589.html
Resolution (31-Oct-2008): competition starts
Tuesday 4-Nov-2008 12:00 noon.
The deadline for submission of tool implementations is one hour before the competition starts.

* what should be the timeout (for all categories, except complexity): 60 sec or 120 sec ?
Deadline: October 30 , 4 p.m. CET.
Resolution: three votes for 60 seconds, two votes for 120 seconds.

* What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk.
Resolution (30-Oct-2008): there is a Coccinelle version that works with coq-8.2beta4

* What is the procedure/deadline for submission of new (public) examples to the TPDB? (13-Oct-2008)
Resolution (30-Oct-2008) no bulk submissions before 1-November deadline. But see next item.

* What about submission of (late/secret) problems? (29-Oct-2008)
Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html

* Are the categories LP and FP part of the upcoming competition?
(13-Oct-2008)
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html

YES.

* Will there be a SRS-certified category?
(10-Oct-2008)

YES

* Will certificates be accepted that are verifiable only with Coq-8.2beta4 (and not with 8.1)?
(10-Oct-2008)
http://lists.lri.fr/pipermail/termtools/2008-October/000514.html

YES

Termination Competition

2025-09-18T09:36:07Z

Ffrohn: /* Organization */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[Term Rewriting|string and term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[C_Complexity|complexity of C programs]]
* termination of [[Term Rewriting|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[Cycle_Rewriting|termination of cycle rewriting]]
* [[Probabilistic_Rewriting|termination of probabilistic term rewriting]] (since 2024)

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2025]] affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], [https://termcomp.github.io/Y2025/ Results].
* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration].

* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]

* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]

* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Termination Competition 2025

2025-09-08T09:09:55Z

Ffrohn: /* Live Results */

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/Y2025/ Results]

== Dates ==

* Tool and Benchmark Submission: <s>August 6</s> August 13, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* We will 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, we will 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.

Termination Competition

2025-09-08T08:36:05Z

Ffrohn: /* History of Termination Competitions */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn. Jobs are run on Star-Exec.

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[Term Rewriting|string and term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[C_Complexity|complexity of C programs]]
* termination of [[Term Rewriting|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[Cycle_Rewriting|termination of cycle rewriting]]
* [[Probabilistic_Rewriting|termination of probabilistic term rewriting]] (since 2024)

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2025]] affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], [https://termcomp.github.io/Y2025/ Results].
* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration].

* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]

* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]

* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Termination Competition 2025

2025-09-03T10:11:32Z

Ffrohn:

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.

== Live Results ==
[https://termcomp.verify.rwth-aachen.de/Y2025/ Live Results]

== Dates ==

* Tool and Benchmark Submission: <s>August 6</s> August 13, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* We will 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, we will 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.

Termination Competition 2025 technical details

2025-08-25T06:49:52Z

Ffrohn: /* General */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.
* If your solver needs to write to temporary files, write them to <code>/tmp</code>. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

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

== Certification ==

We use CeTA version 3.6 for certification.

Termination Competition 2025 technical details

2025-08-25T06:49:09Z

Ffrohn: /* General */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.
* If your solver needs to write to temporary files, write them to `/tmp`. Other directories might be read-only, or shared between instances, resulting in unpredictable behavior.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

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

== Certification ==

We use CeTA version 3.6 for certification.

C Programs

2025-08-19T14:41:35Z

Ffrohn: /* Proposed semantics */

[[Category:Categories]]

== Proposed semantics ==

* The starting point is the main function without arguments.

* Functions which are only declared, but not defined, are considered to be terminating, have no side effects, and return a non-deterministic value according to the function's return type.

* The special (and only declared) function __VERIFIER_nondet_String() returns a non-deterministic C String, i.e., a pointer to some freshly allocated memory where the last byte of this allocation is the value '\0' (we may provide a standard implementation for this function, but provers are allowed to hard-code its semantics).

* The function exit(int) terminates the execution of the program.

* In C, memory-unsafe programs can behave arbitrarily. Therefore, neither YES nor NO is a correct result for programs violating memory safety. So a proof of memory safety needs to be part of a termination proof. If there is interest for that, we could also offer an additional category where memory safety can be assumed and where no programs are allowed which might violate memory safety.

* We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.

* Integer division by negative numbers is assumed to be done by truncation towards zero (as in the C99 standard and no implementation-defined behavior as in the C89 standard).

* We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior. Moreover, read access to allocated, but uninitialized memory is assumed to just return a non-deterministic value.

* We assume the following sizes of primitive data types:
bool: 8 bit
char: 8 bit
short: 16 bit
int: 32 bit
long: 64 bit
float: 32 bit
double: 64 bit
pointer: 64 bit

* Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program
int main(){
int x = 0;
while( x++ == x );
}
: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code>P</code> where the execution of <code>gcc -c -std=c99 -Wsequence-point P</code> shows a warning.

* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).

* Time limit: 300 seconds.

== See also ==

Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

Termination Competition 2025

2025-08-05T10:05:11Z

Ffrohn: /* Dates */

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.



== Dates ==

* Tool and Benchmark Submission: <s>August 6</s> August 13, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* We will 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, we will 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.

Termination Competition 2025 technical details

2025-07-30T20:25:06Z

Ffrohn:

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

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

== Certification ==

We use CeTA version 3.6 for certification.

Termination Competition 2025 technical details

2025-07-30T08:28:45Z

Ffrohn:

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

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

Termination Competition 2025 technical details

2025-07-24T13:47:02Z

Ffrohn: /* Testing Locally */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec --writable-tmpfs -C --bind $TPDB:$TPDB $image solver --timeout=$timeout --category=$category $TPDB/$benchmark
</code>
where $TPDB is the path to your clone of the TPDB.

In my case, I get:

<code>
apptainer exec --writable-tmpfs -C --bind $WORK/benchmarks/TPDB:$WORK/benchmarks/TPDB loat.sif solver --timeout=60 --category=Integer_Transition_Systems $WORK/benchmarks/TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-07-24T13:37:59Z

Ffrohn: /* Execution Environment */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

Resource limits:
* 4 cores
* 60s wallclock time
* 20.345 MiB RAM

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec solver --timeout=60 --category=$category $benchmark
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --timeout=60 --category=Integer_Transition_Systems TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025

2025-07-24T13:35:27Z

Ffrohn: /* Changes with respect to 2024 */

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.



== Dates ==

* Tool and Benchmark Submission: August 6, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* We will 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, we will 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.

Termination Competition 2025

2025-07-24T13:35:05Z

Ffrohn: /* Changes with respect to 2024 */

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.



== Dates ==

* Tool and Benchmark Submission: August 6, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* We will 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.

Termination Competition 2025

2025-07-24T13:34:48Z

Ffrohn: /* Changes with respect to 2024 */

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.



== Dates ==

* Tool and Benchmark Submission: August 6, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.
* 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.

Termination Competition 2025

2025-06-02T11:54:42Z

Ffrohn: /* Registration */

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.



== Dates ==

TBA


== 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]].


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 [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ 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.

Termination Competition 2025 technical details

2025-05-21T11:18:22Z

Ffrohn:

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer run $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec solver --timeout=60 --category=$category $benchmark
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --timeout=60 --category=Integer_Transition_Systems TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:58:17Z

Ffrohn: /* Execution Environment */

Termination Competition 2025 technical details

2025-05-21T10:50:21Z

Ffrohn: /* Lessons Learned from Testing */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. The competition will run using Apptainer (which can run both Apptainer and Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:49:08Z

Ffrohn: /* Execution Environment */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. The competition will run using Apptainer (which can run both Apptainer and Docker images). During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

=== Docker - Apptainer incompatibilities ===

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:48:29Z

Ffrohn: /* Lessons Learned from Testing */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

=== Docker - Apptainer incompatibilities ===

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:48:16Z

Ffrohn: /* Docker -- Apptainer incompatibilities */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

=== Docker -- Apptainer incompatibilities ===

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:48:04Z

Ffrohn: /* Lessons Learned from Testing */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

= Docker -- Apptainer incompatibilities =

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-21T10:47:35Z

Ffrohn: /* Execution Environment */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Apptainer or Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-15T22:16:54Z

Ffrohn: /* Lessons Learned from Testing */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''amd64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-14T15:00:44Z

Ffrohn: /* Lessons Learned from Testing */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''arm64-architecture'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025 technical details

2025-05-14T14:59:58Z

Ffrohn:

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Lessons Learned from Testing ==

First tests already revealed several pitfalls:

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.
* The image must be for an '''arm64-architecture'''

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025

2025-05-05T07:25:33Z

Ffrohn: /* Technical Details */

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.



== Dates ==

TBA


== 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]].


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.

Termination Competition 2025

2025-05-05T07:25:13Z

Ffrohn: /* Competition Procedure */

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.



== Dates ==

TBA


== 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]].


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 will be made 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.

Termination Competition 2025 technical details

2025-04-11T08:16:59Z

Ffrohn: Created page with "== Execution Environment == Starting from 2025, TermComp runs on the RWTH HPC cluster. Tools must be submitted as Docker images. During the competition, the following two co..."

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. During the competition, the following two commands will be executed in your 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 must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Termination Competition 2025

2025-04-09T16:29:26Z

Ffrohn: /* Changes with respect to 2024 */

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.



== Dates ==

TBA


== 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 will be made available [[Termination Competition 2025 technical details|here]] soon.


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 will be made 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.

Termination Competition 2025

2025-04-09T15:41:14Z

Ffrohn: /* Changes with respect to 2024 */

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.



== Dates ==

TBA


== 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 will be made available [[Termination Competition 2025 technical details|here]] soon.


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 will be made 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.

Proposed changes:

* We plan to use [http://cl-informatik.uibk.ac.at/isafor/cpf3.html CPF 3]
* 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.