Difference between revisions of "Termination Competition 2021"
(→Contact: updated termtools address) |
(Link to the result (should have done earlier!!)) |
||
| (2 intermediate revisions by one other user not shown) | |||
| Line 6: | Line 6: | ||
<!-- FF I didn't know where this part fits in: as well as contributions in bug reports --> | <!-- FF I didn't know where this part fits in: as well as contributions in bug reports --> | ||
| − | |||
== Status == | == Status == | ||
[https://termcomp.github.io/Y2021/ Final Result] | [https://termcomp.github.io/Y2021/ Final Result] | ||
| − | |||
| − | |||
== Dates == | == Dates == | ||
| Line 19: | Line 16: | ||
* Bugfix Deadline: July 10 | * Bugfix Deadline: July 10 | ||
* Final Run: July 13 | * Final Run: July 13 | ||
| − | * Presentation of Results: | + | * Presentation of Results: July 15 |
== Competition Categories and Awards == | == Competition Categories and Awards == | ||
| Line 73: | Line 70: | ||
* Jürgen Giesl, RWTH Aachen | * Jürgen Giesl, RWTH Aachen | ||
* Georg Moser, University of Innsbruck | * Georg Moser, University of Innsbruck | ||
| − | * Albert Rubio | + | * Albert Rubio, Complutense University of Madrid |
| − | * Akihisa Yamada (Organizer), AIST Tokyo Waterfront | + | * Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront |
== Registration == | == Registration == | ||
Latest revision as of 06:44, 14 July 2021
In 2021, the Termination and Complexity Competition will be affiliated with CADE.
The competition will be run on the StarExec platform. The first run will be shortly before CADE, followed by a bug/conflict reporting phase and allowance for bug fixes. The final run and a presentation of the final results will be live at CADE.
Contents
Status
Dates
- Tool and Problem Submission: June 30
- First Run: July 1
- Bug/Conflict Report Deadline: July 5
- Bugfix Deadline: July 10
- Final Run: July 13
- Presentation of Results: July 15
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 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 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).
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline. The SC will decide what should be penalized, depending on the discussion among the participants.
Steering Committee
- Florian Frohn, MPI Saarbrücken
- Jürgen Giesl, RWTH Aachen
- Georg Moser, University of Innsbruck
- Albert Rubio, Complutense University of Madrid
- Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront
Registration
To submit a tool, please follow the instruction at the TermCOMP web repository.
To submit a benchmark, please follow the instruction at TPDB repository.
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 or Complexity in particular.
- user guide
- issue tracker
- announcements and discussion (combined feed for recent messages)
- (obsolete) announcements and discussion (discontinued, but contains some information that is still valid and not available elsewhere)
Technical Details
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
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.
