Difference between revisions of "Termination Competition 2018"
(→Competition Categories: Info on new category proposals.) |
(→Registration: explained registration proc.) |
||
Line 53: | Line 53: | ||
* 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] | * 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] | ||
− | * *and* with the competition's organizer, A. Yamada (so I know what solver/configuration to use). | + | * *and* with the competition's organizer, A. Yamada (so I know what solver/configuration to use). |
− | + | Please let me know by email which category you want to participate, and the startexec IDs of your account, your tool, and a configuration per category (if decided). | |
− | |||
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 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. |
Revision as of 01:55, 31 May 2018
In 2018, the Termination and Complexity Competition will be affiliated with the Federated Logic Conference (FLOC 2018). The competition will be run on the StarExec platform.
Contents
Dates
- Tool Registration: June 8, 2018
- Problem Submission: June 15, 2018
- Updates of Registered Tools: June 29, 2018
- Competition: July 13-14, 2018
Competition Categories
The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...)
Proposals for new categories are welcome and will be discussed in the mailing list.
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 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 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.
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
- Johannes Waldmann, HTWK Leipzig, Germany (advisory)
- Akihisa Yamada, NII, Japan
Registration
Participants must register
- 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
- *and* with the competition's organizer, A. Yamada (so I know what solver/configuration to use).
Please let me know by email which category you want to participate, and the startexec IDs of your account, your tool, and a configuration per category (if decided).
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.
- user guide
- announcements and discussion (combined feed for recent messages)
- announcements and discussion (discontinued, but contains some information that is still valid and not available elsewhere)
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 star-exec-presenter - developed and running 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 johannes.waldmann<at>htwk-leipzig.de
Send new problems for the competition to akihisayamada<at>nii.ac.jp
Changes with respect to 2017
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.