View source for Termination and Complexity Competition 2016

From Termination-Portal.org

← Termination and Complexity Competition 2016

You do not have permission to edit this page, for the following reason:

---

You can view and copy the source of this page.

In 2016, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] and it will take place "live" during the workshop. Participants may give a short presentation of their tool during the competition session at the workshop. The competition will be run on the [http://www.starexec.org/ StarExec platform]. == Dates == * Tool Registration: July 31, 2016 (detail: [[Termination_Competition_2016_Registration]]) * Problem Submission: August 14, 2016 * Updates of Registered Tools: August 21, 2016 * Competition: September 5-6, 2016 == 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, ...) == 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 [[Termination_Competition_Problem_Selection_Algorithm]]. The selection is made so that the whole competition will be executed live during the competition session of WST 2016. There might be modifications of the rules suggested by the organizer and decided by the SC. The wall-clock timeout will be 30 seconds, and 4 cores will be available (if a tool wants to use concurrent execution). A longer timeout for selected categories might be possible and has to be negotiated with the participants of that category. 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. <!-- 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 * René Thiemann, Universität Innsbruck, Austria * Johannes Waldmann, HTWK Leipzig, Germany Organizing Commmittee * Johannes Waldmann, HTWK Leipzig, Germany (StarExec) * René Thiemann, Universität Innsbruck, Austria (CPF) * Akihisa Yamada, Universität Innsbruck, Austria (TPDB) == Registration == Participants must register * 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 they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec] * *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]] 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 [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] * [http://starexec.lefora.com/directory announcements and discussion] ([http://starexec.lefora.com/feed/get/type/rss/source/domain/id/280028 combined feed for recent messages]) * [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/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running 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 johannes.waldmann<at>htwk-leipzig.de Send new problems for the competition to rene.thiemann<at>uibk.ac.at == Changes with respect to 2015 == 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: * The CPF version is in the process of being updated from version 2.3 to version 2.4. This transition consists mainly of incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log]. The only non-incremental change is that now there is a dedicated input format for termination problems modulo AC, which before have been encoded as relative termination problems. <!-- == TODO == See [[Termination Competition 2015 TODO]] -->

Return to Termination and Complexity Competition 2016.