In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].

== Dates (tentative) ==

* call for tools, certifiers, problems: May 26
* registration of tools: June 15
* updates of registered tools, submission of problems: July 1
* competition runs: July 15 - 21
* results announced: July 21, during the Second FLoC Olympic Games Award Ceremony, Vienna.

== Competition Categories and Awards ==

The competition contains several categories, grouped in three meta-categories:

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

In each meta-category, a medal will be awarded to the highest-scoring solver.

For every meta-category, we consider the sum of the scores for each category within that meta-category:
The score of a tool is determined by the number of other tools which could be beaten in that category.

This puts the emphasis on categories with many competitors.
(In particular, a category with just one entrant would produce a zero score.)
A category is only run at the competition if there are at least 2 participants and at least 40 examples
for this category in the underlying termination problem data base.

== New Categories ==

This year a new category on termination of C programs will be included (see the details [http://www.termination-portal.org/wiki/C_Programs here]).

Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.

== 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 (link http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm), however because of moving to [http://www.starexec.org StarExec], 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).

For nearly all categories, the tools will be started in their directory and obtain two parameters:

* the problem file and
* the timeout in seconds.

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
* Stefan von der Krone, HTWK Leipzig, Germany

== Registration Info (tentative) ==

Participants must register on [http://www.starexec.org StarExec], and send an email to the organizers, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].

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.

== Technical Detail ==

We intend to run the competition 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.

Technical details about the execution platform 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

2014-05-26T09:48:37Z

Albert: Created page with "We will fix some number "c" with 0 < c < 1. This number indicates the percentage of problems to be taken from each family. So in principle, we would like to choose c * |F| pro..."

We will fix some number "c" with 0 < c < 1. This number indicates the percentage of problems to be taken from each family. So in principle, we would like to choose c * |F| problems from each family F. Here, |F| is the number of problems in the family F.

In order to avoid problems with very large or very small families, there will be two additional numbers "a" and "b" with 0 < a < b. Here, "a" is the minimum number of examples that should be chosen from each family. Similarly, "b" is the maximum number of examples that should be chosen from each family.

To illustrate this, let c = 1/2 and let a = 10 and b = 100. Then for a family F with 50 problems, we would randomly choose c * |F| = 25 problems from the family F. For a family F with 16 problems, we would not choose c * |F| = 8 problems, because this number would be smaller than a = 10. Instead, we would choose a = 10 problems randomly. For a family with 300 problems, we would not choose c * |F| = 150 problems, because this number would be larger than b = 100. Instead, we would choose b = 100 problems randomly.

To summarize, for every family F, we randomly choose:

c * |F| problems, if a <= c*|F| <= b
a problems, if c*|F| < a
b problems, if b < c*|F|

This rule is applied to every family with the same numbers a,b,c.

The numbers "a", "b" and "c" will be chosen such that the competition can complete in time, which depends on the number of new TPDB submissions and participants. (The numbers have been a = 10, b = 75, c = 0.3 in the last year.)

Termination Competition 2014

2014-05-26T09:44:31Z

Albert:

Termination Competition 2014 technical details

2014-05-26T09:41:17Z

Albert: Created page with "We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver execution and benchmark library service under joint development (since 2012..."

We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver execution and benchmark library service under joint development (since 2012) at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions.

For displaying the results of the termination competition, we are building a separate web service at HTWK Leipzig.

Here is some information for participants:

* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] NOTE: there may be service interruptions (e.g., sudden changes in benchmark arrangement).
* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html] (UPDATE: this was out of date, the limit is actually 64 GB)
* Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer.
* hardware on starexec: see [https://www.starexec.org/starexec/public/machine-specs.txt] Solvers are run on nodes with 4 cores each.
* software on starexec: RHEL 6.3 (so [http://mirror.nsc.liu.se/centos-store/6.3/isos/x86_64/ Centos 6.3] should be a close match). Package selection, see [http://starexec.forumotion.com/t23-problem-with-dynamic-linking#47]
* java is available on starexec nodes (jdk 1.6.0_41) - see [http://starexec.forumotion.com/t27-install-more-recent-jre-on-nodes] - see also remark on ulimits and -Xmx [http://starexec.forumotion.com/t34-ulimits-settings-may-hurt-java-programs#69]
* it is helpful to follow other solver communities, e.g., [http://smtcomp.sourceforge.net/2014/ SMT COMP 2014]

information on the web GUI (under construction) for presenting results [[Star_Exec_Presenter]]

Separate page with impressions from using the demo version of Star Exec, in 2012: [[Star_Exec_Test]]

Termination Competition 2014

2014-05-26T09:32:23Z

Albert:

In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].

== Dates (tentative) ==

* call for solvers, certifiers, benchmarks: May 20
* registration of solvers: June 15
* updates of registered solvers, submission of benchmarks: July 1
* competition runs: July 15 - 20
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.

== Competition Categories and Awards ==

The competition contains several categories, grouped in meta-categories:

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

In each meta-category, a medal will be awarded to the highest-scoring solver.

For every meta-category, we consider the sum of the scores for each category within that meta-category:
The score of a tool is determined by the number of other tools which could be beaten in that category.

This puts the emphasis on categories with many competitors.
(In particular, a category with just one entrant will produce zero score.)

== Committees ==

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

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany
* Stefan von der Krone, HTWK Leipzig, Germany

== Registration info (tentative) ==

Participants must register on Starexec, and by email to the organizer, indicating the competition categories where they plan to enter solvers and benchmarks, and then upload their contributions to starexec.

We recommended to register early. After the deadline, access to 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 [http://lists.lri.fr/mailman/listinfo/termtools termtools] because that is where announcements will be made, and discussion takes place.

== Technical Detail ==

(this sub-page should move to a separate page)

We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver execution and benchmark library service under joint development (since 2012) at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions.

For displaying the results of the termination competition, we are building a separate web service at HTWK Leipzig.

Here is some information for participants:

* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] NOTE: there may be service interruptions (e.g., sudden changes in benchmark arrangement).
* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html] (UPDATE: this was out of date, the limit is actually 64 GB)
* Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer.
* hardware on starexec: see [https://www.starexec.org/starexec/public/machine-specs.txt] Solvers are run on nodes with 4 cores each.
* software on starexec: RHEL 6.3 (so [http://mirror.nsc.liu.se/centos-store/6.3/isos/x86_64/ Centos 6.3] should be a close match). Package selection, see [http://starexec.forumotion.com/t23-problem-with-dynamic-linking#47]
* java is available on starexec nodes (jdk 1.6.0_41) - see [http://starexec.forumotion.com/t27-install-more-recent-jre-on-nodes] - see also remark on ulimits and -Xmx [http://starexec.forumotion.com/t34-ulimits-settings-may-hurt-java-programs#69]
* it is helpful to follow other solver communities, e.g., [http://smtcomp.sourceforge.net/2014/ SMT COMP 2014]

information on the web GUI (under construction) for presenting results [[Star_Exec_Presenter]]

Separate page with impressions from using the demo version of Star Exec, in 2012: [[Star_Exec_Test]]

== Contact ==

To contact the steering committee of the termination competition, send email to terminationcompetitionsc<at>lists.rwth-aachen.de.
The competition organizers can be reached at termcomp<at>htwk-leipzig.de