Difference between revisions of "Termination Competition 2019"

From Termination-Portal.org
Jump to navigationJump to search
(→‎Result: new url)
 
(9 intermediate revisions by 3 users not shown)
Line 1: Line 1:
−
We intend to be part of [https://tacas.info/toolympics.php Toolympics],
+
In 2019, the Termination and Complexity Competition will be affiliated with [https://tacas.info/toolympics.php Toolympics],
−
with results presented during TACAS'19, April 16-17, Prague.
+
with results presented during [https://conf.researchr.org/track/etaps-2019/tacas-2019-papers TACAS 2019], April 7, Prague.
  
−
We intend to run on Starexec. The actual run will take
+
 
−
place a few weeks/days before presentation of results,
+
The competition will be run on the [http://www.starexec.org/ StarExec platform],
 +
a few weeks/days before the presentation of results,
 
at the discretion of the organizer, Akihisa Yamada.
 
at the discretion of the organizer, Akihisa Yamada.
 +
 +
== Result ==
 +
 +
[https://termcomp.github.io/Y2019/ Result]
 +
 +
== Dates  ==
 +
 +
* Tool and Problem Submission: <s>March 15, 2019</s> March 16, 2019 (AoE)
 +
* Communication of Initial Results: March 22, 2019
 +
* Finalization of Results: March 31, 2019
 +
* Presentation: April 7, 2019
 +
 +
== 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, ...)
 +
 +
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].
 +
 +
<!-- maybe not this year
 +
The competition categories are 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.
 +
 +
The scoring follows [[Termination Competition 2014]]:
 +
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.
 +
 +
 +
== Competition Procedure ==
 +
 +
All participants in the same category will be run on
 +
the existing problems of this category.
 +
<!-- 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 FSCD 2017.  -->
 +
There might be modifications of the rules suggested by the organizer and decided by the SC.
 +
 +
The wall-clock timeout will be 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 by -10 points.
 +
However, we will try to accept bugfixes if they are sufficiently in advance to the finalization of results.
 +
 +
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
 +
* Albert Rubio (chair), UPC Barcelona, Spain
 +
* Christian Sternagel, Universität Innsbruck, Austria
 +
* Johannes Waldmann, HTWK Leipzig, Germany
 +
* Akihisa Yamada, NII, Japan
 +
 +
Organizing Commmittee
 +
* Akihisa Yamada, NII, Japan
 +
 +
== Registration ==
 +
 +
Participants must be registered 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  you plan to enter tools and problems, and then upload your contributions to [http://www.starexec.org StarExec]
 +
 +
Then, please email the competition's organizer (A. Yamada)
 +
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category. Participants of the previous competition can just indicate so if they want to participate to the same categories.
 +
 +
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]
 +
* (new in 2019) [https://github.com/StarExec/StarExec/issues issue tracker]
 +
* [https://www.tapatalk.com/groups/starexec/index.php announcements and discussion] ([https://www.tapatalk.com/groups/starexec/app.php/feed combined feed for recent messages])
 +
* (obsolete) [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/AkihisaYamada/starexec-master starexec-master]
 +
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).
 +
 +
Technical details about the execution platform (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 akihisayamada<at>nii.ac.jp.
 +
 +
Send new problems for the competition to akihisayamada<at>nii.ac.jp
 +
 +
== Changes with respect to 2018 ==
 +
 +
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:  -->
 +
 +
<!--
 +
== TODO ==
 +
 +
See [[Termination Competition 2016 TODO]]
 +
-->

Latest revision as of 09:25, 12 June 2020

In 2019, the Termination and Complexity Competition will be affiliated with Toolympics, with results presented during TACAS 2019, April 7, Prague.


The competition will be run on the StarExec platform, a few weeks/days before the presentation of results, at the discretion of the organizer, Akihisa Yamada.

Result

Result

Dates

  • Tool and Problem Submission: March 15, 2019 March 16, 2019 (AoE)
  • Communication of Initial Results: March 22, 2019
  • Finalization of Results: March 31, 2019
  • Presentation: April 7, 2019

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

Proposals for new categories are welcome and will be discussed in the mailing list.


A category is only run at the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base.


Competition Procedure

All participants in the same category will be run on the existing problems of this category. There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 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 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 by -10 points. However, we will try to accept bugfixes if they are sufficiently in advance to the finalization of results.

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
  • Albert Rubio (chair), UPC Barcelona, Spain
  • Christian Sternagel, Universität Innsbruck, Austria
  • Johannes Waldmann, HTWK Leipzig, Germany
  • Akihisa Yamada, NII, Japan

Organizing Commmittee

  • Akihisa Yamada, NII, Japan

Registration

Participants must be registered on Starexec (so you can upload and test your solver): enter your data at StarExecRegistration, indicating the competition categories where you plan to enter tools and problems, and then upload your contributions to StarExec

Then, please email the competition's organizer (A. Yamada) indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category. Participants of the previous competition can just indicate so if they want to participate to the same categories.

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.

StarExec Information

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

Technical Detail

The competition will be running 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.

Competition data will be presented via starexec-master (a successor of star-exec-presenter developed at HTWK Leipzig).

Technical details about the execution platform (as of 2014) 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 akihisayamada<at>nii.ac.jp.

Send new problems for the competition to akihisayamada<at>nii.ac.jp

Changes with respect to 2018

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.



Retrieved from "http://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2019&oldid=1845"