Difference between revisions of "Termination Competition 2014"

From Termination-Portal.org
Jump to navigationJump to search
 
(43 intermediate revisions by 5 users not shown)
Line 1: Line 1:
 
In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].
 
In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].
  
== Dates (tentative) ==
+
== Current News ==
 +
 
 +
Competition results at [http://nfa.imn.htwk-leipzig.de/termcomp-2014/competition/20] . Demonstration results  at [http://nfa.imn.htwk-leipzig.de/termcomp-2014/competition/23]. [[Termination Competition 2014 Questionnaire]]. Also, check the mailing list [http://lists.lri.fr/pipermail/termtools/2014-July/thread.html]
 +
 
 +
== Dates ==
  
 
* call for tools, certifiers, problems: May 26
 
* call for tools, certifiers, problems: May 26
 
* registration of tools: June 15
 
* registration of tools: June 15
 
* updates of registered tools, submission of problems: July 1
 
* updates of registered tools, submission of problems: July 1
* competition runs: July 15 - 20
+
* competition runs: July 19 - 21
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.
+
* results announced: July 21, during the Second FLoC Olympic Games Award Ceremony, Vienna.
  
 
== Competition Categories and Awards ==
 
== Competition Categories and Awards ==
Line 23: Line 27:
  
 
This puts the emphasis on categories with many competitors.
 
This puts the emphasis on categories with many competitors.
(In particular, a category with just one entrant will produce a zero score.)
+
(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 ==
+
== New Categories ==
  
This year a new category on termination of C programs will be included (see the deatils [http://www.termination-portal.org/wiki/C_Programs here]).
+
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.
 
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 ==
+
== Competition Procedure ==
  
All participants on 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 (link). The number of problems is not fixed and will depend on the number of existing problems. The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrrent execution).
+
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.
  
For nearly all categories, the tools will be started in their directory and obtain two parameters, first the problem-file and second, 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.
+
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 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 afterwards the new results but out of competition).
+
For nearly all categories, the tools will be started in their directory and obtain two parameters:
  
For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non
+
* the problem file and
contradictory answers minus the given penalization (if any).
+
* the timeout in seconds. - UPDATE Thu Jun 12 16:56:23 CEST 2014: one parameter (problem file name) on the command line, extra info from environment variables, see [[Termination Competition 2014 technical details]]
  
Problem selection algorithm will be the same as previous years (link http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm), however because of moving to starexec, there might be modifications of the rules
+
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.
suggested by the organizer and sanctioned by the SC".
+
 
 +
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 ==
 
== Committees ==
Line 49: Line 58:
 
Steering Committee
 
Steering Committee
 
* Jürgen Giesl, RWTH Aachen, Germany
 
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Reunion
+
* Frederic Mesnard, Université de la Réunion, France
 
* Albert Rubio (chair), UPC Barcelona, Spain
 
* Albert Rubio (chair), UPC Barcelona, Spain
 
* Rene Thiemann, Universität Innsbruck, Austria
 
* Rene Thiemann, Universität Innsbruck, Austria
Line 58: Line 67:
 
* Stefan von der Krone, HTWK Leipzig, Germany
 
* Stefan von der Krone, HTWK Leipzig, Germany
  
== Registration info (tentative) ==
+
== Registration ==
 +
 
 +
Participants must register on [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].
 +
 
 +
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.
  
Participants must register on Starexec, and by email to the organizer, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to 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.
  
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 the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.
  
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.
+
== Registration (Detail) ==
 +
 
 +
see this page: [[Termination Competition 2014 Registration]]
 +
 
 +
== StarExec Wiki ==
 +
 
 +
Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].
  
 
== Technical Detail ==
 
== Technical Detail ==
Line 70: Line 89:
 
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.
 
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]
+
Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].
  
 
== Contact ==
 
== Contact ==
  
To contact the steering committee of the termination competition, send email to terminationcompetitionsc<at>lists.rwth-aachen.de.  
+
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 termcomp<at>htwk-leipzig.de
+
 
 +
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Latest revision as of 13:45, 11 October 2015

In 2014, the Termination Competition will be part of the FLoC Olympic Games.

Current News

Competition results at [1] . Demonstration results at [2]. Termination Competition 2014 Questionnaire. Also, check the mailing list [3]

Dates

  • call for tools, certifiers, problems: May 26
  • registration of tools: June 15
  • updates of registered tools, submission of problems: July 1
  • competition runs: July 19 - 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 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 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 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 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 certified (see also the CPF-website) and complexity categories. See all existing 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

Participants must register on StarExecRegistration, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to StarExec.

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 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 termtools mailing list, because that is where announcements will be made, and where discussion takes place.

Registration (Detail)

see this page: Termination Competition 2014 Registration

StarExec Wiki

Lots of useful information about StarExec is available here.

Technical Detail

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