Termination-Portal.org - User contributions [en]

20th International Workshop on Termination

2025-04-14T13:26:02Z

Thiemann: change HTWK Leipzig URL to more concrete WST 2025 website

The 20th Intl. Workshop on Termination will take place at [https://www.imn.htwk-leipzig.de/~waldmann/WST2025/ HTWK Leipzig, Germany], in early September 2025. [https://www.imn.htwk-leipzig.de/~waldmann/ Johannes Waldmann] is the local organizer.

TPDB

2016-12-02T11:18:01Z

Thiemann: updated link to converter

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

== Syntax and semantics specification ==

* 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 ==
* version 9.0 (2014), 10.3 (2015) 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 ==

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

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.

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

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

Tools:CeTA

2016-09-06T10:25:02Z

Thiemann: Updated members of CeTA developers

{{Tool
|shortname=CeTA
|longname=Certified Termination Analysis
|homepage=http://cl-informatik.uibk.ac.at/software/ceta/
|country=Austria
|university=LFU Innsbruck
|developers=http://cl-informatik.uibk.ac.at/software/ceta/members.php
|publication=[[Bibtex:TS09|Certification of Termination Proofs using CeTA]]
}}


CeTA maintains a [http://cl-informatik.uibk.ac.at/software/ceta/#introduction list of supported techniques], moreover also the
[http://cl-informatik.uibk.ac.at/software/ceta/versions.php differences between the various CeTA versions] are described.

Termination and Complexity Competition 2016

2016-08-08T08:33:55Z

Thiemann: Akihisa Yamada takes care of TPDB submissions

In 2016, the Termination and Complexity Competition  will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] and it will take place "live" during the workshop. Participants may give a short presentation of their tool during the competition session at the workshop. The competition will be run on the [http://www.starexec.org/ StarExec platform].

== Dates ==

* Tool Registration: July 31, 2016 (detail: [[Termination_Competition_2016_Registration]])
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution). A longer timeout for selected categories might be possible and has to be negotiated with the participants of that category.

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (CPF)
* Akihisa Yamada, Universität Innsbruck, Austria (TPDB)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Information ==

this refers to StarExec in general, and not to Termination in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [http://starexec.lefora.com/directory announcements and discussion] ([http://starexec.lefora.com/feed/get/type/rss/source/domain/id/280028 combined feed for recent messages])
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to akihisa.yamada<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

Termination and Complexity Competition 2016

2016-08-08T08:33:29Z

Thiemann: Akihisa Yamada takes care of TPDB submissions

In 2016, the Termination and Complexity Competition  will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] and it will take place "live" during the workshop. Participants may give a short presentation of their tool during the competition session at the workshop. The competition will be run on the [http://www.starexec.org/ StarExec platform].

== Dates ==

* Tool Registration: July 31, 2016 (detail: [[Termination_Competition_2016_Registration]])
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution). A longer timeout for selected categories might be possible and has to be negotiated with the participants of that category.

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (CPF)
* Akihisa Yamada, Universität Innsbruck, Austria (TPDB)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Information ==

this refers to StarExec in general, and not to Termination in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [http://starexec.lefora.com/directory announcements and discussion] ([http://starexec.lefora.com/feed/get/type/rss/source/domain/id/280028 combined feed for recent messages])
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

News:Termination and Complexity Competition 2016

2016-07-09T17:06:05Z

Thiemann: entry for competition 2016

{{News
|text=The [[Termination and Complexity Competition 2016]] will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ Workshop on Termination in 2016].
|date=Sep 5 or Sep 6, 2016
}}

Termination and Complexity Competition 2016

2016-07-08T17:37:28Z

Thiemann:

In 2016, the Termination and Complexity Competition  will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] and it will take place "live" during the workshop. Participants may give a short presentation of their tool during the competition session at the workshop. The competition will be run on the [http://www.starexec.org/ StarExec platform].

== Dates ==

* Tool Registration: July 31, 2016
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

Termination and Complexity Competition 2016

2016-07-08T17:34:39Z

Thiemann: removed preliminary disclaimer

In 2016, the Termination and Complexity Competition 
will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination].

== Dates ==

* Tool Registration: July 31, 2016
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

Termination and Complexity Competition 2016

2016-07-08T07:35:50Z

Thiemann: No Awards

== IMPORTANT: THIS IS A PRELIMINARY WEBSITE TO BE DISCUSSED BY THE SC ==

In 2016, the Termination and Complexity Competition 
will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination].

== Dates ==

* Tool Registration: July 31, 2016
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

Termination Competition 2016

2016-07-07T12:48:56Z

Thiemann: Thiemann moved page Termination Competition 2016 to Termination and Complexity Competition 2016

#REDIRECT [[Termination and Complexity Competition 2016]]

Termination and Complexity Competition 2016

2016-07-07T12:48:56Z

Thiemann: Thiemann moved page Termination Competition 2016 to Termination and Complexity Competition 2016

== IMPORTANT: THIS IS A PRELIMINARY WEBSITE TO BE DISCUSSED BY THE SC ==

In 2016, the Termination and Complexity Competition 
will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination].

== Dates ==

* Tool Registration: July 31, 2016
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

== Competition Categories and Awards ==

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

Termination and Complexity Competition 2016

2016-07-07T12:48:32Z

Thiemann: Draft version of termination and complexity competition 2016

== IMPORTANT: THIS IS A PRELIMINARY WEBSITE TO BE DISCUSSED BY THE SC ==

In 2016, the Termination and Complexity Competition 
will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination].

== Dates ==

* Tool Registration: July 31, 2016
* Problem Submission: August 14, 2016
* Updates of Registered Tools: August 21, 2016
* Competition: September 5-6, 2016

== Competition Categories and Awards ==

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

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016.
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* René Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2015 ==

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:

* The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems.

News:Workshop on Termination 2016: September 5-7 at Computational Logic in the Alps

2016-05-02T11:58:24Z

Thiemann: Thiemann moved page News:Workshop on Termination 2016: September 5-6 at Computational Logic in the Alps to News:Workshop on Termination 2016: September 5-7 at Computational Logic in the Alps: corrected date of WST 2016

{{News
|text= The [http://cl-informatik.uibk.ac.at/events/wst-2016/ Workshop on Termination in 2016] is part of [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps].
|date= Sep 5-7, 2016
}}

News:Workshop on Termination 2016: September 5-6 at Computational Logic in the Alps

2016-05-02T11:58:24Z

#REDIRECT [[News:Workshop on Termination 2016: September 5-7 at Computational Logic in the Alps]]

News:Workshop on Termination 2016: September 5-7 at Computational Logic in the Alps

2016-05-02T11:57:56Z

Thiemann: Corrected Date of WST 2016

{{News
|text= The [http://cl-informatik.uibk.ac.at/events/wst-2016/ Workshop on Termination in 2016] is part of [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps].
|date= Sep 5-7, 2016
}}

WST

2016-05-02T11:57:19Z

Thiemann: corrected date of WST 2016

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:
* [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.

Information about previous workshops can be found online:
* [http://vsl2014.at/wst/ 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014
* Joint Workshop on Termination [http://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
* [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]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 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]]

News:Workshop on Termination 2016: September 5-7 at Computational Logic in the Alps

2016-05-02T11:51:38Z

Thiemann: Adding WST 2016

{{News
|text= The [http://cl-informatik.uibk.ac.at/events/wst-2016/ Workshop on Termination in 2016] is part of [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps].
|date= Sep 5-6, 2016
}}

WST

2016-05-02T11:41:32Z

Thiemann: link to WST 2016 and CLA 2016 pages

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:
* [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-6, 2016.

Information about previous workshops can be found online:
* [http://vsl2014.at/wst/ 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014
* Joint Workshop on Termination [http://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
* [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]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 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]]

TPDB

2015-10-14T14:19:40Z

Thiemann: inserted correct TPDB version for termComp 2015

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

== Syntax and semantics specification ==

* 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 ==
* version 9.0 (2014), 10.3 (2015) 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 ==

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

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.

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://termcomp.uibk.ac.at/current/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

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

TPDB

2015-07-09T11:00:39Z

Thiemann: /* Data */

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

== Syntax and semantics specification ==

* 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 ==
* version 9.0 (2014), 10.? (2015) 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 ==

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

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.

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://termcomp.uibk.ac.at/current/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

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

Termination Competition 2015

2015-07-01T07:33:04Z

Thiemann: /* Contact */

In 2015, the Termination Competition ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation])
will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].

== Dates ==

preliminary:
* registration of tools: July 1
* submission of problems: July 7
* updates of registered tools: July 15

fixed:
* competition runs: August 5 and 6 (during CADE)

== Competition Categories and Awards ==

The competition contains several categories from the areas of

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2014 ==

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:

* The answering scheme and the scoring of the complexity category slightly changed. The new version of the grammar and the updated scoring mechanism are described in more detail on the [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity related page], and below is just a small summary of the changes.
** The grammar for answers was simplified and is now less ambiguous.
** The grammar for answers now explicitly contains lower bounds.
** Lower bounds will be counted for complexity.

Adopted changes:

* The CPF version has been updated from version 2.2 to version 2.3. This transition consists of purely incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log].

* In addition to the category for "full" C programs, we also intend to have a category for "C integer" programs. These are essentially integer transition systems formulated as imperative programs in C syntax. A detailed definition can be found [http://www.termination-portal.org/wiki/C_Integer_Programs here].

Termination Competition 2015

2015-07-01T07:32:31Z

Thiemann: indicate where to send new examples

In 2015, the Termination Competition ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation])
will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].

== Dates ==

preliminary:
* registration of tools: July 1
* submission of problems: July 7
* updates of registered tools: July 15

fixed:
* competition runs: August 5 and 6 (during CADE)

== Competition Categories and Awards ==

The competition contains several categories from the areas of

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new examples for the competition to rene.thiemann<at>uibk.ac.at

== Changes with respect to 2014 ==

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:

* The answering scheme and the scoring of the complexity category slightly changed. The new version of the grammar and the updated scoring mechanism are described in more detail on the [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity related page], and below is just a small summary of the changes.
** The grammar for answers was simplified and is now less ambiguous.
** The grammar for answers now explicitly contains lower bounds.
** Lower bounds will be counted for complexity.

Adopted changes:

* The CPF version has been updated from version 2.2 to version 2.3. This transition consists of purely incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log].

* In addition to the category for "full" C programs, we also intend to have a category for "C integer" programs. These are essentially integer transition systems formulated as imperative programs in C syntax. A detailed definition can be found [http://www.termination-portal.org/wiki/C_Integer_Programs here].

Termination Competition 2015

2015-06-24T13:41:17Z

Thiemann: Changes in CPF and in complexity

In 2015, the Termination Competition ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation])
will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].

== Dates ==

preliminary:
* registration of tools: July 1
* submission of problems: July 7
* updates of registered tools: July 15

fixed:
* competition runs: August 5 and 6 (during CADE)

== Competition Categories and Awards ==

The competition contains several categories from the areas of

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

== Changes with respect to 2014 ==

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:

* The answering scheme and the scoring of the complexity category slightly changed. The new version of the grammar and the updated scoring mechanism are described in more detail on the [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity related page], and below is just a small summary of the changes.
** The grammar for answers was simplified and is now less ambiguous.
** The grammar for answers now explicitly contains lower bounds.
** Lower bounds will be counted for complexity.

Adopted changes:

* The CPF version has been updated from version 2.2 to version 2.3. This transition consists of purely incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log].

Termination Competition 2015

2015-06-06T07:50:29Z

Thiemann:

In 2015, the Termination Competition will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].

== Dates ==

preliminary:
* registration of tools: July 1
* submission of problems: July 7
* updates of registered tools: July 15

fixed:
* competition runs: August 5 and 6 (during CADE)

== Competition Categories and Awards ==

The competition contains several categories from the areas of

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

== Changes with respect to 2014 ==

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:

*

Adopted changes:

*

Termination Competition 2015

2015-06-06T07:40:50Z

Thiemann: changed submission of tool deadline

In 2015, the Termination Competition will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].

== Dates ==

preliminary:
* registration of tools: July 1
* submission of problems: July 8
* updates of registered tools: July 15

fixed:
* competition runs: August 5 and 6 (during CADE)

== Competition Categories and Awards ==

The competition contains several categories from the areas of

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years [[Termination_Competition_Problem_Selection_Algorithm]]
There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

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

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

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.

== StarExec Wiki ==

Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

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

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

== Changes with respect to 2014 ==

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:

*

Adopted changes:

*

TPDB

2014-07-31T07:35:08Z

Thiemann: /* Syntax and semantics specification */

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

== Syntax and semantics specification ==

* 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 ==
* version 9.0 (2014) 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 ==

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

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.

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://termcomp.uibk.ac.at/current/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

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

TPDB

2014-07-31T07:34:19Z

Thiemann: fixed links which now point into repository for TPDB

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd xtc.xsd], available within 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 ==
* version 9.0 (2014) 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 ==

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

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.

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://termcomp.uibk.ac.at/current/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

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

TPDB

2014-07-31T07:28:30Z

Thiemann: changed link from termcomp into TPDB-repository

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd xtc.xsd], available within 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 ==
* version 9.0 (2014) 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 ==

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

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.

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/current/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

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

XTC Format Specification

2014-07-31T07:14:34Z

Thiemann: /* Schema */

= Schema =
The schema <tt>xtc.xsd</tt> is part of the termination problem database ([http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB]) in the subdirectory <tt>xml</tt>. The schema can be inspected
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd within the browser] or
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd downloaded].

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
There are stylesheets to transform the XML-files into HTML or ASCII (the old TPDB format). Both stylesheets are contained in the TPDB, subdirectory <tt>xml</tt>.
* converter to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl]
* converter to ASCII: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl]

XTC Format Specification

2014-07-31T07:13:52Z

Thiemann: /* Schema */

= Schema =
The schema <tt>xtc.xsd</tt> is part of the termination problem database ([http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB]). The schema can be inspected
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd within the browser] or
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd downloaded].

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
There are stylesheets to transform the XML-files into HTML or ASCII (the old TPDB format). Both stylesheets are contained in the TPDB, subdirectory <tt>xml</tt>.
* converter to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl]
* converter to ASCII: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl]

XTC Format Specification

2014-07-31T07:13:01Z

Thiemann: corrected link to XSL-transformations

= Schema =
The schema <tt>xtc.xsd</tt> is part of the termination problem database. The schema can be inspected
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd within the browser] or
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd downloaded].

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
There are stylesheets to transform the XML-files into HTML or ASCII (the old TPDB format). Both stylesheets are contained in the TPDB, subdirectory <tt>xml</tt>.
* converter to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl]
* converter to ASCII: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl]

XTC Format Specification

2014-07-31T07:03:49Z

Thiemann: /* Schema */

= Schema =
The schema <tt>xtc.xsd</tt> is part of the termination problem database. The schema can be inspected
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd within the browser] or
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd downloaded].

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow.

XTC Format Specification

2014-07-31T07:03:30Z

Thiemann: Correct link to schema

= Schema =
The schema <tt>xtc.xsd</tt> is part of the termination problem database. The file can be inspected
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/tip/xml/xtc.xsd within the browser] or
[http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd downloaded].

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow.

Termination Competition

2014-07-24T08:25:43Z

Thiemann: /* History of Termination Competitions */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the 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 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marche, [http://www.lri.fr/~marche/termination-competition/ Paris].
Since 2008 the competition was run by Rene Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
For 2014, we intend to move to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2014|Termination Competition 2014]] will be part of [http://vsl2014.at/olympics/ FLoC Olympic Games].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|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)
Extensions under consideration for 2014
* [[C Programs]]
* [[Transition Systems]]
Longer term plans
* [[ITRS|integer term rewriting]]

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== 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 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 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]

TPDB

2014-07-04T09:34:33Z

Thiemann: Added link to new to TPDB location

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* 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 ==
* version 9.0 (2014) 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 ==

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

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.

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/current/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

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

TPDB

2014-06-12T11:30:58Z

Thiemann: fixed links to more recent versions of converter

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* 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 ==
* 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 ==

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

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.

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/current/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

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

Tools:CeTA

2014-05-07T17:14:59Z

Thiemann: add links to feature list of CeTA

{{Tool
|shortname=CeTA
|longname=Certified Termination Analysis
|homepage=http://cl-informatik.uibk.ac.at/software/ceta/
|country=Austria
|university=LFU Innsbruck
|developers=[[People:Christian Sternagel|Christian Sternagel]], [[People:René Thiemann|René Thiemann]], and [[People:Harald Zankl|Harald Zankl]]
|publication=[[Bibtex:TS09|Certification of Termination Proofs using CeTA]]
}}


CeTA maintains a [http://cl-informatik.uibk.ac.at/software/ceta/#introduction list of supported techniques], moreover also the
[http://cl-informatik.uibk.ac.at/software/ceta/versions.php differences between the various CeTA versions] are described.

TPDB

2014-02-24T13:38:47Z

Thiemann: /* Data */

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* 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 ==
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2013) 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 ==

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

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.

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/status/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

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

News:Termination Competition 2013: June 24 - June 26

2013-07-03T11:54:39Z

Thiemann: Created page with "{{News |text=The Termination Competition 2013 took place "live" during the [http://rta2013.few.vu.nl RTA conference]. |date=June 24 - June 26, 2013 }}"

{{News
|text=The [[Termination Competition 2013]] took place "live" during the [http://rta2013.few.vu.nl RTA conference].
|date=June 24 - June 26, 2013
}}

Termination Competition

2013-07-03T11:48:51Z

Thiemann:

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the 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 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007 the competition was hosted in [http://www.lri.fr/~marche/termination-competition/ Paris].
Since 2008 the competition is hosted in [http://termcomp.uibk.ac.at Innsbruck].

== Upcoming Competitions ==

The [[Termination_Competition_2013|Termination Competition 2013]] will be run during the
[http://www.win.tue.nl/rdp2013/ RDP 2013 Conference].

The long-term plan is to move the termination competition to the [[Star_Exec|Star Exec]] platform.

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|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)
Planned extensions:
* [[ITRS|integer term rewriting]] (under consideration)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

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

TPDB

2013-07-03T11:46:59Z

Thiemann:

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* 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 ==
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2013) 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.* (2008 .. 2009) http://dev.aspsimon.org/workspace/projectdownloads/tpdb-5.0.2.tar.gz
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/status/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

Termination Competition 2013

2013-06-17T15:34:48Z

Thiemann:

The Termination Competition 2013 will be run during the [http://www.win.tue.nl/rdp2013/ RDP 2013 Conference] (June 23 - June 28).

The competition will be hosted
on the [http://termcomp.uibk.ac.at Termcomp Platform] at Institute of
Computer Science, University of Innsbruck,
Austria.

Results will be presented during the conference.

Important Dates

* Software requests: May 27 2013, 13:01 CEST
* Problem submission: June 10 2013, 13:01 CEST
* Tool submission: June 19 2013, 13:01 CEST
* Competition start: June 24 2013, 09:00 CEST

Further information can be found on the [http://termcomp.uibk.ac.at/2013/rules.html 2013 competition site of the Termcomp Platform].

TPDB

2012-07-10T08:04:16Z

Thiemann:

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

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* 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 ==
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), and 8.0.6 (2012) 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.* (2008 .. 2009) http://dev.aspsimon.org/workspace/projectdownloads/tpdb-5.0.2.tar.gz
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/

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

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

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/status/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

Termination Competition

2012-07-09T14:34:56Z

Thiemann:

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the 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 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007 the competition was hosted in [http://www.lri.fr/~marche/termination-competition/ Paris].
Since 2008 the competition is hosted in [http://termcomp.uibk.ac.at Innsbruck].

== Upcoming Competitions ==

The [[Termination_Competition_2012|Termination Competition 2012]] is a satellite event of [http://ijcar.cs.manchester.ac.uk/ IJCAR] (June 26 - July 1).

The long-term plan is to move the termination competition to the [[Star_Exec|Star Exec]] platform.

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|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)
Planned extensions:
* [[ITRS|integer term rewriting]] (under consideration)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

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

Termination Competition 2012 Comments

2012-06-29T04:07:39Z

Thiemann: updated numbers after end of competition

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert has a higher score (108) than matchbox-uncert (103) which is interesting. Johannes, can you please explain.
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* AProVE and AProVE-CeTA have the same YES-count (141) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop).

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 62 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 39 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 35 % for full rewriting and 20 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Java Bytecode =
* The example "Overflow.jar" was chosen. However, its termination depends on the handling of integers. If integers are implemented like in Java (i.e. their range is bounded), this example does not terminate (for any input). Maybe we should remove this (and other examples whose termination behaviour depends on the implementation of bounded integers)?

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ_10/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof. CF As far as I recall, AProVE generated a proof of this size for this example already in the competition of 2010. For obvious reasons, I do not dare to check this on TermComp right now.

Termination Competition 2012 Comments

2012-06-28T11:32:49Z

Thiemann:

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain. ((July 27, 10:48)
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (111) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop). (July 27, 10:48)

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Java Bytecode =
* The example "Overflow.jar" was chosen. However, its termination depends on the handling of integers. If integers are implemented like in Java (i.e. their range is bounded), this example does not terminate (for any input). Maybe we should remove this (and other examples whose termination behaviour depends on the implementation of bounded integers)?

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ_10/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof.

Termination Competition 2012 Comments

2012-06-28T08:49:21Z

Thiemann:

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain. ((July 27, 10:48)
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (111) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop). (July 27, 10:48)

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof.

News:Termination Competition 2012: June 26 - June 29

2012-06-28T08:46:58Z

Thiemann:

{{News
|text=The [[Termination Competition 2012]] takes place "live" during the [http://ijcar.cs.manchester.ac.uk/ IJCAR conference]. You can also read or write [[Termination_Competition_2012_Comments]].
|date=June 26 - June 29, 2012
}}

Termination Competition 2012 Comments

2012-06-28T08:45:09Z

Thiemann:

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain.
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (109) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop).

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof.

Termination Competition 2012 Comments

2012-06-28T08:39:56Z

Thiemann:

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain.
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (109) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop).

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.