http://termination-portal.org/mediawiki/api.php?action=feedcontributions&feedformat=atom&user=GieslTermination-Portal.org - User contributions [en]2026-05-14T04:28:59ZUser contributionsMediaWiki 1.34.2http://termination-portal.org/mediawiki/index.php?title=User_talk:Eleanore.meyer&diff=2068User talk:Eleanore.meyer2025-09-10T08:24:59Z<p>Giesl: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [https://www.mediawiki.org/wiki/Special:MyLanguage/Help:Contents help pages].<br />
Again, welcome and have fun! [[User:Giesl|Giesl]] ([[User talk:Giesl|talk]]) 08:24, 10 September 2025 (UTC)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=TPDB&diff=2047TPDB2025-06-18T11:49:20Z<p>Giesl: TPDB-ARI (since is the only version which also contains the probabilistic TRS examples)</p>
<hr />
<div>The Termination Problems Data Base collects termination problems<br />
that are being used in termination competitions.<br />
<br />
== Syntax and semantics specification ==<br />
<br />
* for versions from 11.* onwards (XML format): [https://github.com/TermCOMP/TPDB/raw/master/xml/xtc.xsd xtc.xsd], already part of the [https://github.com/TermCOMP/TPDB TPDB]<br />
* for versions from 7.* onwards (XML format): [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd xtc.xsd], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB]<br />
* for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html<br />
<br />
see also:<br />
<br />
* output specification for certified categories: http://cl-informatik.uibk.ac.at/software/cpf/<br />
<br />
== Data ==<br />
* version 11.0 (2019): https://github.com/TermCOMP/TPDB-ARI<br />
* version 9.0 (2014), 10.3 (2015), 10.4 (2016), 10.5 (2017), 10.6 (2018) http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB<br />
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2012) and 8.0.7 (2013) http://termcomp.uibk.ac.at/status/downloads/<br />
* version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz<br />
* version 5.0.2 (2008..2009) http://termcomp.uibk.ac.at/termcomp/docs/tpdb-5.0.2.tar.gz<br />
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/<br />
<br />
== Sources ==<br />
<br />
TPDB problems are collected from a variety of sources, by a variety of contributors. Often, the author of the problem is not the creator of the respective TPDB file. Sometimes, TPDB file structure (directory names) have been changed.<br />
<br />
The following are references for classical problem sets that appear in TPDB. <br />
<br />
* TRS/SK90 Joachim Steinbach, Ulrich Kühler: Check your Ordering - termination proofs and open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990.<br />
* TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf<br />
* TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps<br />
* SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?). They include (as z027 .. z064) a set of one-rule termination problems by Alfons Geser (Habilitationsschrift, Tübingen, 2001) and possibly Winfried Kurth (Dissertation, Clausthal, 1990)<br />
<br />
And here are some extra bits of trivia.<br />
<br />
* SRS termination problems ICFP_2010 and ICFP_2010_relative were produced by participants of the ICFP 2010 programming contest, organized by Bertram Felgenhauer and Johannes Waldmann. ''All'' of these problems are terminating by construction. See https://www.imn.htwk-leipzig.de/~waldmann/talk/10/icfp/<br />
<br />
== Tools ==<br />
* converter from pre-7 (textual) format to 7.* (XML) format: http://cl-informatik.uibk.ac.at/users/thiemann/convert.jar, usage:<br />
<br />
java -jar convert.jar someTrs.trs > someTrs.xml <br />
<br />
* converter from 7.* (XML) format to pre-7 (textual) format: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB], usage:<br />
<br />
xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs<br />
<br />
* converter from 7.* (XML) format to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl], see explanation at http://lists.lri.fr/pipermail/termtools/2018-July/001212.html<br />
<br />
* Haskell library for reading and writing TPDB (plain and XML format) [http://hackage.haskell.org/package/tpdb]</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=19th_International_Workshop_on_Termination&diff=195119th International Workshop on Termination2023-08-17T17:02:09Z<p>Giesl: underlined names and added web sites</p>
<hr />
<div>August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria. [https://goo.gl/maps/2Z2ekhg4ftbnLj5o7 (Google Map)]<br />
<br />
As part of [http://cl-informatik.uibk.ac.at/events/osr-2023/ Obergurgl Summer on Rewriting 2023] and<br />
co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].<br />
<br />
<br />
<br />
==Background==<br />
<br />
The Workshop on Termination (WST) traditionally brings together, in an<br />
informal setting, researchers interested in all aspects of termination,<br />
whether this interest be practical or theoretical, primary or derived. <br />
The workshop also provides a ground for cross-fertilization of ideas from <br />
the different communities interested in termination (e.g., working on <br />
computational mechanisms, programming languages, software engineering, <br />
constraint solving, etc.). The friendly atmosphere enables fruitful <br />
exchanges leading to joint research and subsequent publications.<br />
<br />
The 19th International Workshop on Termination (WST 2023) continues<br />
the successful workshops held in<br />
St. Andrews (1993), <br />
La Bresse (1995), <br />
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]), <br />
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]), <br />
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]), <br />
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]), <br />
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]), <br />
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]), <br />
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]), <br />
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),<br />
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]), <br />
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]), <br />
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]), <br />
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),<br />
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),<br />
Oxford ([http://wst2018.webs.upv.es/ 2018]),<br />
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and<br />
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).<br />
<br />
==Workshop Topics==<br />
<br />
The 19th International Workshop on Termination welcomes contributions <br />
on all aspects of termination. In particular, papers investigating applications <br />
of termination (for example in complexity analysis, program analysis and<br />
transformation, theorem proving, program correctness, modeling computational <br />
systems, etc.) are very welcome.<br />
<br />
Topics of interest include (but are not limited to):<br />
<br />
* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)<br />
* abstraction methods in termination analysis<br />
* certification of termination and complexity proofs<br />
* challenging termination problems<br />
* comparison and classification of termination methods<br />
* implementation of termination and complexity methods<br />
* non-termination analysis and loop detection<br />
* normalization and infinitary normalization<br />
* operational termination of logic-based systems<br />
* ordinal notation and subrecursive hierarchies<br />
* SAT, SMT, and constraint solving for (non-)termination analysis<br />
* scalability and modularity of termination methods<br />
* well-founded relations and well-quasi-orders<br />
<br />
==Termination Competition==<br />
<br />
Since 2003, the catalytic effect of WST to stimulate new research<br />
on termination has been enhanced by the celebration of the [[Termination_Competition]] <br />
and its continuously developing problem databases containing thousands of programs <br />
as challenges for termination analysis in different categories.<br />
In 2023, the Termination Competition will run shortly before WST. Tool/benchmark authors are invited to submit a short tool paper and give a presentation on the workshop.<br />
<br />
==Keynote Speaker==<br />
<br />
[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.<br />
<b>Termination of Probabilistic Programs</b><br />
<br />
<b>Abstract</b><br />
Unlike for ordinary programs, termination of probabilistic programs is more nuanced: A probabilistic program can terminate with probability 1 while still needing infinitely many computation steps in expectation. We will explore the complexity landscape of probabilistic program termination and present proof rules for proving both almost-sure termination (i.e. termination with probability 1) as well as positive almost-sure termination (i.e. termination within finite expected time). Time permitting, we will furthermore dive into open problems on termination of weighted programs – a generalization of probabilistic programs where branches can be associated with more general weights from a semiring.<br />
<br />
==Program==<br />
<br />
===Thursday 24 August===<br />
<br />
'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)<br />
{|<br />
|-<br />
|style="vertical-align:top;"|14:00<br />
| [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski]:<br />
'''Termination of Probabilistic Programs <span style="color:red;">(invited talk)</span>'''<br />
|-<br />
|style="vertical-align:top;"|15:00<br />
| <u>Jan-Christoph Kassing</u> and [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]:<br />
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]<br />
|-<br />
|style="vertical-align:top;"|15:30<br />
| coffee break<br />
|}<br />
<br />
'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)<br />
{|<br />
|style="vertical-align:top;"|16:00<br />
| <u>Fabian Mitterwallner</u>, Aart Middeldorp and René Thiemann:<br />
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]<br />
|-<br />
|style="vertical-align:top;"|16:30<br />
| Teppei Saito and Nao Hirokawa:<br />
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]<br />
|-<br />
|style="vertical-align:top;"|17:00<br />
| <u>René Thiemann</u> and Elias Wenninger:<br />
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]<br />
|-<br />
|style="vertical-align:top;"|17:30<br />
| <u>Nao Hirokawa</u> and Aart Middeldorp:<br />
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]<br />
|-<br />
|18:00<br />
|<br />
----<br />
|}<br />
<br />
===Friday 25 August===<br />
<br />
'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)<br />
{|<br />
|style="vertical-align:top;"|9:00<br />
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:<br />
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]<br />
|-<br />
|style="vertical-align:top;"|9:30<br />
| Liye Guo and Cynthia Kop:<br />
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]<br />
|-<br />
|style="vertical-align:top;"|10:00<br />
| Jera Hensel and <u>[https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]</u>:<br />
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]<br />
|-<br />
|style="vertical-align:top;"|10:30<br />
| coffee break<br />
|}<br />
<br />
'''Session 4''': Non-Termination (Chair: René Thiemann)<br />
{|<br />
|style="vertical-align:top;"|11:00<br />
| Dieter Hofbauer and Johannes Waldmann:<br />
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]<br />
|-<br />
|style="vertical-align:top;"|11:30<br />
| <u>[https://ffrohn.github.io Florian Frohn]</u> and [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]:<br />
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]<br />
|-<br />
|style="vertical-align:top;"|12:00<br />
| [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]:<br />
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]<br />
|-<br />
|style="vertical-align:top;"|12:30<br />
| lunch<br />
|}<br />
<br />
'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)<br />
{|<br />
|style="vertical-align:top;"|14:00<br />
| <u>Nils Lommen</u>, Eleanore Meyer and [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]:<br />
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]<br />
|-<br />
|style="vertical-align:top;"|14:30<br />
| Cynthia Kop and Deivid Vale:<br />
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]<br />
|-<br />
|style="vertical-align:top;"|15:00<br />
| '''0th Probabilistic termCOMP'''<br />
|-<br />
|style="vertical-align:top;"|15:30<br />
| coffee break<br />
|}<br />
<br />
'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)<br />
{|<br />
|style="vertical-align:top;"|16:00<br />
| <u>Nils Lommen</u>, Eleanore Meyer and [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]:<br />
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''<br />
|-<br />
|style="vertical-align:top;"|16:15<br />
| <u>[https://ffrohn.github.io Florian Frohn]</u> and [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]:<br />
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''<br />
|-<br />
|style="vertical-align:top;"|16:30<br />
| <u>[https://verify.rwth-aachen.de/giesl/ Jürgen Giesl]</u>, Daniel Cloerkes, Stefan Dollase, [https://ffrohn.github.io Florian Frohn], Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:<br />
'''AProVE 2023'''<br />
|-<br />
|style="vertical-align:top;"|16:45<br />
| Fred Mesnard and <u>[http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]</u>:<br />
'''NTI+cTI: a Logic Programming Termination Analyzer'''<br />
|-<br />
|style="vertical-align:top;"|17:00<br />
| Dieter Hofbauer:<br />
'''MultumNonMulta entering Term Rewriting'''<br />
|-<br />
|style="vertical-align:top;"|17:15<br />
| [https://akihisayamada.github.io/ Akihisa Yamada]:<br />
'''Results of the [[Termination Competition 2023]]'''<br />
|-<br />
|style="vertical-align:top;"|17:30<br />
| '''business meeting'''<br />
|}<br />
<br />
==Submission Guidelines==<br />
<br />
Submissions are short papers/extended abstracts which should not exceed 5 pages.<br />
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers<br />
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.<br />
The accepted papers will be made available electronically before the workshop.<br />
<br />
Papers should be submitted electronically via<br />
[https://easychair.org/my/conference?conf=wst2023 the submission page].<br />
<br />
Please use LaTeX and<br />
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]<br />
to prepare your submission.<br />
<br />
==Important Dates==<br />
<br />
* title and abstract submission: <s>June 1</s><br />
* paper submission: <s>June 8</s><br />
* notification: <s>June 15</s><br />
* final version: <s>July 27</s><br />
* workshop: August 24-25<br />
<br />
==Program Committee==<br />
<br />
* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis<br />
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen<br />
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London<br />
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid<br />
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion<br />
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid<br />
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck<br />
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen<br />
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig<br />
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2023&diff=1931Termination Competition 20232023-05-23T18:46:06Z<p>Giesl: Changed Deadline for WST ABstract</p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with [[WST2023|WST 2023]].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before WST, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at WST.<br />
<br />
All (co-)authors of tools or benchmarks are encouraged (but not required) to give a 5-20min presentation of their contributions at WST 2023.<br />
To do so, we ask for a title and abstract by 15 June via [https://easychair.org/conferences/?conf=wst23 this submission site].<br />
Anyone who sends this in may additionally submit a 1-4 page paper by July 1, to be included in the WST-proceedings (but this is not mandatory).<br />
<br />
== Dates ==<br />
<br />
* June 15: (Optional) Title and Abstract Submission [https://easychair.org/conferences/?conf=wst23 to WST]<br />
* July 1: (Optional) Paper Submission<br />
* Aug. 6: Tool and Benchmark Submission<br />
* Aug. 13: First Run<br />
* Aug. 20: Bugfix Deadline<br />
* Aug. 24 (CET): Final Run<br />
* Aug. 24-25 (CET): WST<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2022 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
<br />
Adopted changes:</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1904Termination Competition 20222022-11-07T14:09:35Z<p>Giesl: Final Result</p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
<br />
Five medals will be awarded:<br />
* Gold, Silver, and Bronze medals go to the top three teams according to a competition-wide ranking.<br />
* Two special medals go to the best two teams in advancing the state of the art.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the [https://sws.cs.ru.nl/WST2022 Workshop of Termination (WST 2022)] on 12 August 2022.<br />
We ask for a title+abstract by 18 June via [https://easychair.org/conferences/?conf=wst22 this submission site]. Anyone who sends this in may additionally submit a 1-2 page paper by July 11, to be included in the WST-proceedings (but this is not mandatory).<br />
<br />
== Status ==<br />
<br />
[https://termcomp.github.io/Y2022/ Final Result]<br />
<br />
== Dates ==<br />
<br />
* <s>June 18</s>: (Optional) <s>Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]</s><br />
* July 24: Tools and Problems Submission Deadline<br />
* July 25: First Run<br />
* July 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. <b>7</b> <s>5</s>: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
Five [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
* Gold, Silver, and Bronze medals go to the top three teams according to a competition-wide ranking. Teams are ranked by the Euclidean norms of the normalized score vector. Each component of the vector is the score of the team in a category, divided by the score of the virtual best solver (VBS) in the category. The VBS records the best (consistent) score for each claim collected at least since 2018.<br />
<br />
* Two special medals go to the best two teams in advancing the state of the art. If a team gets higher score for a benchmark and a claim than previous year's VBS, then the team gets the difference as a special score, and teams are ranked by sums of these scores. In short, if you claim YES/NO while no tool in the past claimed so, then you get special score 1.<br />
<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* A competition-wide ranking scheme based on Euclidean norm.<br />
* Awards for the two best solvers in advancing the state of the art (closing unsolved termination problems or improving known complexity bounds).<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1894Termination Competition 20222022-06-09T15:19:33Z<p>Giesl: </p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
Several medals will be awarded, following a ranking scheme which is to be announced.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the [https://sws.cs.ru.nl/WST2022 Workshop of Termination (WST 2022)] on 12 August 2022.<br />
We ask for a title+abstract by 18 June via [https://easychair.org/conferences/?conf=wst22 this submission site]. Anyone who sends this in may additionally submit a 1-2 page paper by July 11, to be included in the WST-proceedings (but this is not mandatory).<br />
<br />
== Dates ==<br />
<br />
* June 18: Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]<br />
* July 24: Tools and Problems Submission Deadline<br />
* July 25: First Run<br />
* July 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. 5: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
The number of medals and the ranking scheme will be announced soon.<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
* A competition-wide ranking scheme following SMT-COMP<br />
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)<br />
* The best new comer award<br />
* The most improved tool award<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1893Termination Competition2022-06-09T15:18:26Z<p>Giesl: /* History of Termination Competitions */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* The [[Termination Competition 2022]] will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and it will be part of the Olympic Games at the Federated Logic Conference [https://www.floc2022.org/floc-olympic-games FLoC 2022]. <br />
<br />
== Organization ==<br />
<br />
Questions and suggestions regarding the competition<br />
should go to [[Termtools|the termtools mailing list]].<br />
Discussion is open and happens primarily on the list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://ffrohn.github.io], RWTH Aachen<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada] (Chair), AIST Tokyo Waterfront<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].<br />
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1891Termination Competition 20222022-06-02T14:15:03Z<p>Giesl: </p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
Several medals will be awarded, following a ranking scheme which is to be announced.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the [https://sws.cs.ru.nl/WST2022 Workshop of Termination (WST 2022)] on 12 August 2022.<br />
We ask for a title+abstract by 18 June via [https://easychair.org/conferences/?conf=wst22 this submission site], and anyone who sends this in may additionally submit a 1-2 page paper to be included in the proceedings (but this is not mandatory).<br />
<br />
== Dates ==<br />
<br />
* June 18: Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]<br />
* July 24: Tools and Problems Submission Deadline<br />
* July 25: First Run<br />
* July 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. 5: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
The number of medals and the ranking scheme will be announced soon.<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
* A competition-wide ranking scheme following SMT-COMP<br />
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)<br />
* The best new comer award<br />
* The most improved tool award<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1890Termination Competition 20222022-06-01T16:18:33Z<p>Giesl: </p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
Several medals will be awarded, following a ranking scheme which is to be announced.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the [https://sws.cs.ru.nl/WST2022 Workshop of Termination (WST 2022)] on 12 August 2022.<br />
We ask for a title+abstract by 18 June, and anyone who sends this in may additionally submit a 1-2 page paper to be included in the proceedings (but this is not mandatory), deadline somewhere in July.<br />
<br />
== Dates ==<br />
<br />
* June 18: Title and Abstract Submission to WST<br />
* July 24: Tools and Problems Submission Deadline<br />
* July 25: First Run<br />
* July 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. 5: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
The number of medals and the ranking scheme will be announced soon.<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
* A competition-wide ranking scheme following SMT-COMP<br />
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)<br />
* The best new comer award<br />
* The most improved tool award<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1889Termination Competition 20222022-06-01T16:16:07Z<p>Giesl: </p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
Several medals will be awarded, following a ranking scheme which is to be announced.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the [https://sws.cs.ru.nl/WST2022 Workshop of Termination (WST 2022)] on 12 August 2022.<br />
We ask for a title+abstract by 18 June, and anyone who sends this in may additionally submit a 1-2 page paper to be included in the proceedings (but this is not mandatory), deadline somewhere in July.<br />
<br />
== Dates ==<br />
<br />
* June 18: Title and Abstract Submission to WST<br />
* Jul. 24: Tools and Problems Submission Deadline<br />
* Jul. 25: First Run<br />
* Aug. 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. 5: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
The number of medals and the ranking scheme will be announced soon.<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
* A competition-wide ranking scheme following SMT-COMP<br />
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)<br />
* The best new comer award<br />
* The most improved tool award<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2022&diff=1888Termination Competition 20222022-06-01T16:10:39Z<p>Giesl: </p>
<hr />
<div>The Termination and Complexity Competition (termCOMP) 2022 will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and takes part in [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games 2022].<br />
Several medals will be awarded, following a ranking scheme which is to be announced.<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before FLoC, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at FLoC.<br />
<br />
All (co-)authors of tools or benchmarks are invited (but not required) to give a 5-20min presentation of their contributions at the Workshop of Termination (WST 2022) on 12 August 2022.<br />
We ask for a title+abstract by 18 June, and anyone who sends this in may additionally submit a 1-2 page paper to be included in the proceedings (but this is not mandatory), deadline somewhere in July.<br />
<br />
== Dates ==<br />
<br />
* June 18: Title and Abstract Submission to WST<br />
* Jul. 24: Tools and Problems Submission Deadline<br />
* Jul. 25: First Run<br />
* Aug. 30: Conflict/Bug Report Deadline<br />
* Aug. 4: Bugfix Deadline<br />
* Aug. 5: Final Run<br />
* Aug. 9: Award Ceremony at FLoC<br />
* Aug. 12: Presentations at WST<br />
<br />
== Awards and Competition Categories ==<br />
<br />
[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.<br />
The number of medals and the ranking scheme will be announced soon.<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, RWTH Aachen<br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
We recommend to register early, and update information as needed. 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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
== Changes with respect to 2021 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
* A competition-wide ranking scheme following SMT-COMP<br />
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)<br />
* The best new comer award<br />
* The most improved tool award<br />
<br />
Adopted changes:<br />
* Medals will be awarded.<br />
* Tool/benchmark authors are invited to submit a paper and present at WST.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1887Termination Competition2022-06-01T16:09:02Z<p>Giesl: </p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* The [[Termination Competition 2022]] will be affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022] and it will be part of the Olympic Games at the Federated Logic Conference [https://www.floc2022.org/floc-olympic-games FLoC 2022]. <br />
<br />
== Organization ==<br />
<br />
Questions and suggestions regarding the competition<br />
should go to [[Termtools|the termtools mailing list]].<br />
Discussion is open and happens primarily on the list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada] (Chair), AIST Tokyo Waterfront<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2021&diff=1880Termination Competition 20212021-05-19T13:12:37Z<p>Giesl: /* Steering Committee */</p>
<hr />
<div>In 2021, the Termination and Complexity Competition will be affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before CADE, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at CADE.<br />
<!-- FF I didn't know where this part fits in: as well as contributions in bug reports --><br />
<br />
<!--<br />
== Status ==<br />
[https://termcomp.github.io/Y2021/ Final Result]<br />
[https://termcomp.github.io/Y2021-1/ Initial Result]<br />
--><br />
<br />
== Dates ==<br />
<br />
* Tool and Problem Submission: June 30<br />
* First Run: July 1<br />
* Bug/Conflict Report Deadline: July 5<br />
* Bugfix Deadline: July 10<br />
* Final Run: July 13<br />
* Presentation of Results: July 15<br />
<br />
== Competition Categories and Awards ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
<!-- maybe not this year<br />
The competition categories are grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
The scoring follows [[Termination Competition 2014]]:<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
--><br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, MPI Saarbrücken <br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio, Complutense University of Madrid<br />
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
<!-- No changes currently<br />
== Changes with respect to 2019 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
--><br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1879Termination Competition2021-05-19T13:11:52Z<p>Giesl: Akihisa is the new chair, Albert's affiliation has changed</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2021]] will be affiliated with [https://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021].<br />
<br />
== Organization ==<br />
<br />
Questions and suggestions regarding the competition<br />
should go to [[Termtools|the termtools mailing list]].<br />
Discussion is open and happens primarily on the list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada] (Chair), AIST Tokyo Waterfront<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2021&diff=1878Termination Competition 20212021-05-17T06:55:30Z<p>Giesl: Date for Presentation</p>
<hr />
<div>In 2021, the Termination and Complexity Competition will be affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
The first run will be shortly before CADE, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final run and a presentation of the final results will be live at CADE.<br />
<!-- FF I didn't know where this part fits in: as well as contributions in bug reports --><br />
<br />
<!--<br />
== Status ==<br />
[https://termcomp.github.io/Y2021/ Final Result]<br />
[https://termcomp.github.io/Y2021-1/ Initial Result]<br />
--><br />
<br />
== Dates ==<br />
<br />
* Tool and Problem Submission: June 30<br />
* First Run: July 1<br />
* Bug/Conflict Report Deadline: July 5<br />
* Bugfix Deadline: July 10<br />
* Final Run: July 13<br />
* Presentation of Results: July 15<br />
<br />
== Competition Categories and Awards ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
<!-- maybe not this year<br />
The competition categories are grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
The scoring follows [[Termination Competition 2014]]:<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
--><br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, MPI Saarbrücken <br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio (Chair), UPC Barcelona <br />
* Akihisa Yamada (Organizer), AIST Tokyo Waterfront<br />
<br />
== Registration ==<br />
<br />
To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].<br />
<br />
To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de<br />
<br />
To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
<!-- No changes currently<br />
== Changes with respect to 2019 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
--><br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termtools&diff=1867Termtools2020-11-11T21:38:36Z<p>Giesl: </p>
<hr />
<div>The Termtools mailing list has been installed to facilitate discussion about [[:Category:Tools|termination tools]] in general and the [[Termination Competition|termination competition]] in particular. <br />
<br />
You can subscribe via the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ list info page]. The list has an [https://lists.rwth-aachen.de/hyperkitty/list/termtools@lists.rwth-aachen.de/ archive] which contains the e-mails sent from November 2020 onwards. The old archive of the list up to November 2020 is [https://verify.rwth-aachen.de/termtools/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termtools&diff=1866Termtools2020-11-11T21:20:40Z<p>Giesl: </p>
<hr />
<div>The Termtools mailing list has been installed to facilitate discussion about [[:Category:Tools|termination tools]] in general and the [[Termination Competition|termination competition]] in particular. <br />
<br />
You can subscribe via the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ list info page]. The list has an [https://lists.rwth-aachen.de/hyperkitty/list/termtools@lists.rwth-aachen.de/ archive] which contains the e-mails sent from November 2020 onwards. The old archive of the list before November 2020 is [https://verify.rwth-aachen.de/termtools/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termtools&diff=1865Termtools2020-11-11T21:12:20Z<p>Giesl: </p>
<hr />
<div>The Termtools mailing list has been installed to facilitate discussion about [[:Category:Tools|termination tools]] in general and the [[Termination Competition|termination competition]] in particular. <br />
<br />
You can subscribe via the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ list info page]. The list has an [https://lists.rwth-aachen.de/hyperkitty/list/termtools@lists.rwth-aachen.de/ archive] which contains the e-mails sent from November 2020 onwards. The old archive of the list before November 2020 is here.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1859Termination Competition2020-07-02T15:49:53Z<p>Giesl: </p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2020]] will be affiliated with [https://ijcar2020.org/ IJCAR 2020].<br />
<br />
== Organization ==<br />
<br />
Questions and suggestions regarding the competition<br />
should go to [[Termtools|the termtools mailing list]].<br />
Discussion is open and happens primarily on the list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tsukuba<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2020&diff=1849Termination Competition 20202020-06-15T09:31:13Z<p>Giesl: /* Dates */</p>
<hr />
<div>In 2020, the Termination and Complexity Competition will be affiliated with [https://ijcar2020.org/ IJCAR].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform]<br />
shortly before IJCAR, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final results,<br />
as well as contributions in bug reports,<br />
will be reported online at IJCAR.<br />
<br />
== Dates ==<br />
<br />
* Tool and Problem Submission: June 19, 2020 (AoE)<br />
* First Run: June 20<br />
* Bug/Conflict Report Deadline: June 25<br />
* Bugfix Deadline: June 28<br />
* Presentation of Results: July 4<br />
<br />
== Competition Categories and Awards ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
<!-- maybe not this year<br />
The competition categories are grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
The scoring follows [[Termination Competition 2014]]:<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
--><br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, MPI Saarbrücken <br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio (Chair), UPC Barcelona <br />
* Akihisa Yamada (Organizer), AIST Tsukuba<br />
<br />
== Registration ==<br />
<br />
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]<br />
<br />
Then, please email the competition's organizer (A. Yamada)<br />
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category.<br />
Participants of the previous competition can just indicate so if they want to participate in the same categories.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at akihisa.yamada<at>aist.go.jp.<br />
<br />
Send new problems for the competition to the organizer.<br />
<br />
<!-- No changes currently<br />
== Changes with respect to 2019 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
--><br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2020&diff=1843Termination Competition 20202020-05-15T16:09:15Z<p>Giesl: /* Dates */</p>
<hr />
<div>In 2020, the Termination and Complexity Competition will be affiliated with [https://ijcar2020.org/ IJCAR].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform]<br />
shortly before IJCAR, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final results,<br />
as well as contributions in bug reports,<br />
will be reported online at IJCAR.<br />
<br />
== Dates ==<br />
<br />
* Tool and Problem Submission: June 19, 2020 (AoE)<br />
* First Run: June 20<br />
* Bug/Conflict Report Deadline: June 25<br />
* Bugfix Deadline: June 28<br />
* Presentation of Results: July 2 (tentative)<br />
<br />
== Competition Categories and Awards ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
<!-- maybe not this year<br />
The competition categories are grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
The scoring follows [[Termination Competition 2014]]:<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
--><br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, MPI Saarbrücken <br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio (Chair), UPC Barcelona <br />
* Akihisa Yamada (Organizer), AIST Tsukuba<br />
<br />
== Registration ==<br />
<br />
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]<br />
<br />
Then, please email the competition's organizer (A. Yamada)<br />
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category.<br />
Participants of the previous competition can just indicate so if they want to participate in the same categories.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at akihisa.yamada<at>aist.go.jp.<br />
<br />
Send new problems for the competition to the organizer.<br />
<br />
<!-- No changes currently<br />
== Changes with respect to 2019 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
--><br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Transition_Systems&diff=1842Transition Systems2020-05-09T12:33:24Z<p>Giesl: </p>
<hr />
<div>[[Category: Categories]]<br />
<br />
Syntax and semantics of the format are presented in [https://www.microsoft.com/en-us/research/publication/termcomp-proposal-pushdown-systems-as-a-model-for-programs-with-procedures/].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1841Termination Competition2020-05-09T12:12:31Z<p>Giesl: /* Competition Categories */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2020]] will be affiliated with [https://ijcar2020.org/ IJCAR 2020].<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
<br />
Discussion is open and primarily happens on the termtools mailing list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tsukuba<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://group-mmm.org/termination/competitions/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://group-mmm.org/termination/competitions/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are availble [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1840Termination Competition2020-05-09T12:11:59Z<p>Giesl: /* Upcoming Competitions */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2020]] will be affiliated with [https://ijcar2020.org/ IJCAR 2020].<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
<br />
Discussion is open and primarily happens on the termtools mailing list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://group-mmm.org/termination/competitions/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://group-mmm.org/termination/competitions/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are availble [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1839Termination Competition2020-05-09T12:11:42Z<p>Giesl: /* Upcoming Competitions */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2020]] will be afiliated with [https://ijcar2020.org/ IJCAR 2020].<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
<br />
Discussion is open and primarily happens on the termtools mailing list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://group-mmm.org/termination/competitions/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://group-mmm.org/termination/competitions/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are availble [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2020&diff=1838Termination Competition 20202020-05-09T12:09:33Z<p>Giesl: </p>
<hr />
<div>In 2020, the Termination and Complexity Competition will be affiliated with [https://ijcar2020.org/ IJCAR].<br />
<br />
The competition will be run on the [http://www.starexec.org/ StarExec platform]<br />
shortly before IJCAR, followed by a bug/conflict reporting phase and allowance for bug fixes.<br />
The final results,<br />
as well as contributions in bug reports,<br />
will be reported online at IJCAR.<br />
<br />
== Dates ==<br />
<br />
* Tool and Problem Submission: June 19, 2020 (AoE)<br />
* First Run: June 20<br />
* Bug/Conflict Report Deadline: June 25<br />
* Bugfix Deadline: June 28<br />
* Finalization of Results: July 1<br />
<br />
== Competition Categories and Awards ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
<!-- maybe not this year<br />
The competition categories are grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
The scoring follows [[Termination Competition 2014]]:<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
--><br />
<br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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).<br />
<br />
A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.<br />
The SC will decide what should be penalized, depending on the discussion among the participants.<br />
<br />
== Steering Committee ==<br />
<br />
* Florian Frohn, MPI Saarbrücken <br />
* Jürgen Giesl, RWTH Aachen <br />
* Georg Moser, University of Innsbruck <br />
* Albert Rubio (Chair), UPC Barcelona <br />
* Akihisa Yamada (Organizer), AIST Tsukuba<br />
<br />
== Registration ==<br />
<br />
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]<br />
<br />
Then, please email the competition's organizer (A. Yamada)<br />
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category.<br />
Participants of the previous competition can just indicate so if they want to participate in the same categories.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
This refers to StarExec in general, and not to Termination or Complexity in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [https://github.com/StarExec/StarExec/issues issue tracker]<br />
* [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])<br />
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Details ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]<br />
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at akihisa.yamada<at>aist.go.jp.<br />
<br />
Send new problems for the competition to the organizer.<br />
<br />
<!-- No changes currently<br />
== Changes with respect to 2019 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
--><br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_Steering_Committee&diff=1833Termination Competition Steering Committee2019-10-21T10:30:49Z<p>Giesl: </p>
<hr />
<div>The basic ideas are:<br />
* one research group hosts (implements, executes) the competition<br />
* a committee, representing all research groups, influences the design and the running of the competition.<br />
<br />
Currently, the Competition is hosted on StarExec.<br />
<br />
The Competition Committee currently<br />
consists of<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
[[Termination_Competition_Steering_Committee_Bylaws]]<br />
<br />
The steering committee assembled on June 3rd, 2009,<br />
during the Workshop on Termination in Leipzig.<br />
<br />
[[TC_SC_Meeting_WST09]]<br />
<br />
= Current Votes =<br />
<br />
<br />
<br />
= Proposed Votes =<br />
<br />
The Competition Committee should vote on ...<br />
(give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)<br />
<br />
= Earlier Votes / Issues resolved otherwise =<br />
<br />
(otherwise = These topics were discussed on the mailing list,<br />
some solution emerged and no-one objected.)<br />
<br />
<br />
* (asked 31-Oct-2008) what is the timeout that will be applied<br />
for verification (by coqc) of the termination certificates:<br />
<br />
<poll><br />
Timemout for verification<br />
1 minute<br />
3 minutes<br />
10 minutes<br />
</poll><br />
<br />
deadline for voting: Monday 3-Nov 12:00 noon CET. <br />
<br />
See discussion at http://lists.lri.fr/pipermail/termtools/2008-October/000594.html<br />
<br />
Resolution: 1 minute timeout.<br />
<br />
* When should the competition start? (asked 30-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000589.html<br />
Resolution (31-Oct-2008): competition starts<br />
Tuesday 4-Nov-2008 12:00 noon.<br />
The deadline for submission of tool implementations is one hour before the competition starts.<br />
<br />
<br />
* what should be the timeout (for all categories, except complexity): 60 sec or 120 sec ? <br />
Deadline: October 30 , 4 p.m. CET. <br />
Resolution: three votes for 60 seconds, two votes for 120 seconds.<br />
<br />
<br />
* What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk. <br />
Resolution (30-Oct-2008): there is a Coccinelle version that works with coq-8.2beta4<br />
<br />
* What is the procedure/deadline for submission of new (public) examples to the TPDB? (13-Oct-2008)<br />
Resolution (30-Oct-2008) no bulk submissions before 1-November deadline. But see next item.<br />
<br />
* What about submission of (late/secret) problems? (29-Oct-2008)<br />
Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html<br />
<br />
* Are the categories LP and FP part of the upcoming competition?<br />
(13-Oct-2008)<br />
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html<br />
<br />
YES. <br />
<br />
* Will there be a SRS-certified category?<br />
(10-Oct-2008)<br />
<br />
YES<br />
<br />
* Will certificates be accepted that are verifiable only with Coq-8.2beta4 (and not with 8.1)?<br />
(10-Oct-2008)<br />
http://lists.lri.fr/pipermail/termtools/2008-October/000514.html<br />
<br />
YES</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_Steering_Committee&diff=1832Termination Competition Steering Committee2019-10-21T10:30:04Z<p>Giesl: </p>
<hr />
<div>The basic ideas are:<br />
* one research group hosts (implements, executes) the competition<br />
* a committee, representing all research groups, influences the design and the running of the competition.<br />
<br />
Currently, the Competition is hosted on StarExec.<br />
<br />
The Competition Committee currently<br />
consists of<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [http://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
<br />
[[Termination_Competition_Steering_Committee_Bylaws]]<br />
<br />
The steering committee assembled on June 3rd, 2009,<br />
during the Workshop on Termination in Leipzig.<br />
<br />
[[TC_SC_Meeting_WST09]]<br />
<br />
= Current Votes =<br />
<br />
<br />
<br />
= Proposed Votes =<br />
<br />
The Competition Committee should vote on ...<br />
(give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)<br />
<br />
= Earlier Votes / Issues resolved otherwise =<br />
<br />
(otherwise = These topics were discussed on the mailing list,<br />
some solution emerged and no-one objected.)<br />
<br />
<br />
* (asked 31-Oct-2008) what is the timeout that will be applied<br />
for verification (by coqc) of the termination certificates:<br />
<br />
<poll><br />
Timemout for verification<br />
1 minute<br />
3 minutes<br />
10 minutes<br />
</poll><br />
<br />
deadline for voting: Monday 3-Nov 12:00 noon CET. <br />
<br />
See discussion at http://lists.lri.fr/pipermail/termtools/2008-October/000594.html<br />
<br />
Resolution: 1 minute timeout.<br />
<br />
* When should the competition start? (asked 30-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000589.html<br />
Resolution (31-Oct-2008): competition starts<br />
Tuesday 4-Nov-2008 12:00 noon.<br />
The deadline for submission of tool implementations is one hour before the competition starts.<br />
<br />
<br />
* what should be the timeout (for all categories, except complexity): 60 sec or 120 sec ? <br />
Deadline: October 30 , 4 p.m. CET. <br />
Resolution: three votes for 60 seconds, two votes for 120 seconds.<br />
<br />
<br />
* What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk. <br />
Resolution (30-Oct-2008): there is a Coccinelle version that works with coq-8.2beta4<br />
<br />
* What is the procedure/deadline for submission of new (public) examples to the TPDB? (13-Oct-2008)<br />
Resolution (30-Oct-2008) no bulk submissions before 1-November deadline. But see next item.<br />
<br />
* What about submission of (late/secret) problems? (29-Oct-2008)<br />
Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html<br />
<br />
* Are the categories LP and FP part of the upcoming competition?<br />
(13-Oct-2008)<br />
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html<br />
<br />
YES. <br />
<br />
* Will there be a SRS-certified category?<br />
(10-Oct-2008)<br />
<br />
YES<br />
<br />
* Will certificates be accepted that are verifiable only with Coq-8.2beta4 (and not with 8.1)?<br />
(10-Oct-2008)<br />
http://lists.lri.fr/pipermail/termtools/2008-October/000514.html<br />
<br />
YES</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1831Termination Competition2019-10-21T10:28:38Z<p>Giesl: /* Competition Categories */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the Termination Workshop 2003 (Valencia),<br />
the community then decided to install an annual termination competition, and to collect benchmarks,<br />
to spur the development of tools and new termination techniques.<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.<br />
From 2018 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.<br />
<br />
== Upcoming Competitions ==<br />
<br />
* [[Termination Competition 2019]] is planned to be part of [https://tacas.info/toolympics.php Toolympics], with results presented during TACAS'19, April 7, Prague.<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
<br />
Discussion is open and primarily happens on the termtools mailing list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken<br />
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://group-mmm.org/termination/competitions/Y2019/ Results].<br />
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://group-mmm.org/termination/competitions/Y2018/ Results].<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)<br />
were run on the laptop computers of their developers in the room. Termination problems were announced <br />
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program<br />
could solve it, they shouted "solved".<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are availble [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=User_talk:Davidkor&diff=1830User talk:Davidkor2019-07-03T12:03:23Z<p>Giesl: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:Giesl|Giesl]] ([[User talk:Giesl|talk]]) 14:03, 3 July 2019 (CEST)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination-Portal.org:About&diff=1817Termination-Portal.org:About2018-10-14T10:22:47Z<p>Giesl: /* Impressum */</p>
<hr />
<div>= Impressum =<br />
Die Ansprechperson für Termination-Portal.org ist:<br />
Jürgen Giesl<br />
Lehr- und Forschungsgebiet Informatik 2<br />
RWTH Aachen University<br />
52074 Aachen<br />
+49 241 80 21230<br />
[mailto:giesl@informatik.rwth-aachen.de giesl@informatik.rwth-aachen.de]<br />
<br />
= Präambel =<br />
Termination-Portal.org ist eine Webseite von und für Forscher aus dem Bereich der Terminierungsanalyse.<br />
Die Idee ist, dass die Seitenbetreiber sich im Regelfall nur um die technischen Voraussetzungen kümmern, während<br />
die Inhalte von den Benutzern, d.h. den Forschern, beigesteuert werden. Dadurch soll<br />
eine ständig aktualisierte Wissenbasis rund um den Forschungsbereich entstehen. <br />
<br />
= Nutzungsbedingungen =<br />
Die Benutzer sind verpflichtet, alle Inhalte, die sie zu dieser Website beisteuern, nach bestem Wissen zu erstellen.<br />
Jeder Benutzer ist für die von ihm erstellten Beiträge selbst in vollem Umfang verantwortlich. Insbesondere muss er beim<br />
Einstellen von Inhalten das Urheberrecht berücksichtigen. Auch Links auf externe Webseiten sind vor dem Einstellen nach<br />
bestem Wissen und Gewissen auf Freiheit von Rechtsverstößen zu prüfen.<br />
<br />
= Haftung für Inhalte =<br />
Die Inhalte dieser Webseite werden von den Benutzern mit großer Sorgfalt erstellt. <br />
Für die Richtigkeit, Vollständigkeit und Aktualität der Inhalte kann jedoch keine Gewähr übernommen werden.<br />
<br />
Die von den Benutzern eingestellten Inhalte können nicht regelmäßig auf mögliche Rechtsverstöße überwacht werden.<br />
Sollten den Seitenbetreibern jedoch Rechtsverstöße bekannt sein bzw. zur Kenntnis gebracht werden, werden die fraglichen<br />
Inhalte umgehend entfernt oder gesperrt.<br />
<br />
= Haftung für Links =<br />
Auf den Inhalt von verlinkten externen Webseiten besteht kein Einfluss. Deshalb kann auch<br />
keine Verantwortung für deren Inhalte übernommen werden. Sollten den Seitenbetreibern jedoch Rechtsverstöße im Inhalt der<br />
externen Seiten bekannt sein bzw. zur Kenntnis gebracht werden, werden die fraglichen Links umgehend entfernt.<br />
<br />
= Datenschutz =<br />
Auf dieser Webseite werden personenbezogene Daten stets auf freiwilliger Basis und im Regelfall durch den Benutzer selbst erhoben. <br />
Der Nutzung jeglicher veröffentlichter personenbezogener Daten sowie die Nutzung der im Impressum veröffentlichten Kontaktdaten<br />
zu Werbezwecken wird hiermit ausdrücklich widersprochen.</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2018&diff=1792Termination Competition 20182018-06-10T12:42:52Z<p>Giesl: Deadline Extension</p>
<hr />
<div>In 2018, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [https://www.floc2018.org/ Federated Logic Conference (FLOC 2018)]. The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: June 15, 2018<br />
* Problem Submission: June 22, 2018 <br />
* Updates of Registered Tools: June 29, 2018 <br />
* Competition: July 13-14, 2018<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Christian Sternagel, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Akihisa Yamada, NII, Japan<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (advisory)<br />
* Akihisa Yamada, NII, Japan<br />
<br />
== Registration ==<br />
<br />
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]<br />
<br />
Then, please email the competition's organizer (A. Yamada)<br />
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category (if decided). Participants of the previous competition can just indicate so if they want to participate to the same categories.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
this refers to StarExec in general, and not to Termination in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [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])<br />
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to akihisayamada<at>nii.ac.jp<br />
<br />
== Changes with respect to 2017 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition&diff=1784Termination Competition2018-05-08T10:54:41Z<p>Giesl: /* Annual International Termination Competition */</p>
<hr />
<div>= Annual International Termination Competition =<br />
<br />
During the 90's a number of new, powerful termination methods<br />
was developed. Thus, at the beginning of the millennium<br />
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].<br />
<br />
After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,<br />
the community decided to install an annual termination competition<br />
to spur the development of tools and new termination techniques.<br />
<br />
From 2004 till 2007, the competition organizer was Claude March&eacute;, [http://www.lri.fr/~marche/termination-competition/ Paris].<br />
From 2008 to 2013 the competition was run by Ren&eacute; Thiemann, [http://termcomp.uibk.ac.at Innsbruck].<br />
Since 2014, the competition organizer is Johannes Waldmann. Jobs are run on the [https://www.starexec.org/ Star Exec] platform at U Iowa. Results are aggregated and displayed at [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 HTWK Leipzig].<br />
<br />
== Upcoming Competitions ==<br />
[[Termination Competition 2018]]<br />
<br />
== Competition Categories ==<br />
<br />
Currently, the competition features the following categories:<br />
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]<br />
* [[Logic_Programming|termination of logic programs]]<br />
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)<br />
* [[Functional_Programming|termination of functional programs]] (since 2007)<br />
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)<br />
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)<br />
* [[Higher_Order|termination of higher order rewriting]] (since 2010)<br />
* [[C_Programs|termination of C programs]] (since 2014)<br />
* termination of [[Transition_Systems|integer transition systems]] (since 2014)<br />
* [[ITRS|integer term rewriting]] (since 2014)<br />
* [[C_Integer_Programs|termination of C integer programs]]<br />
* [[Cycle_Rewriting|termination of cycle rewriting]]<br />
<br />
<br />
Discussion is open and primarily happens on the termtools mailing list.<br />
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members<br />
* [http://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen<br />
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona<br />
* [http://cl-informatik.uibk.ac.at/users/griff/ Christian Sternagel], U. Innsbruck<br />
* [https://www.imn.htwk-leipzig.de/~waldmann/ Johannes Waldmann], HTWK Leipzig<br />
* [http://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo<br />
<br />
== Termination Problems Data Base ==<br />
<br />
The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions. <br />
<br />
We welcome problem submissions from non-participants.<br />
<br />
== History of Termination Competitions ==<br />
<br />
The following competitions have taken place:<br />
<br />
* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration]. <br />
<br />
* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]<br />
<br />
* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]<br />
<br />
* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]<br />
<br />
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]<br />
<br />
* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]<br />
<br />
* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]<br />
<br />
* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results] <br />
<br />
* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]<br />
<br />
* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]<br />
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]<br />
<br />
== Static Backups of Results ==<br />
<br />
For many previous competitions, static backups of the results are availble [https://aprove-developers.github.io/termcomp_results/ here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2018&diff=1783Termination Competition 20182018-05-08T10:52:31Z<p>Giesl: </p>
<hr />
<div>In 2018, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [https://www.floc2018.org/ Federated Logic Conference (FLOC 2018)]. The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: June 8, 2018<br />
* Problem Submission: June 15, 2018 <br />
* Updates of Registered Tools: June 29, 2018 <br />
* Competition: July 13-14, 2018<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
All participants in the same category will be run on<br />
the existing problems of this category.<br />
<!-- 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. --><br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Christian Sternagel, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Akihisa Yamada, NII, Japan<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (advisory)<br />
* Akihisa Yamada, NII, Japan<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the competition's organizer, A. Yamada (so I know what solver/configuration to use). Details will be announced here: [[Termination Competition 2018 Registration]]<br />
<br />
Note: if I (A. Yamada) 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).<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
this refers to StarExec in general, and not to Termination in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [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])<br />
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to akihisayamada<at>nii.ac.jp<br />
<br />
== Changes with respect to 2017 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2017&diff=1778Termination Competition 20172018-04-27T09:25:39Z<p>Giesl: </p>
<hr />
<div>In 2017, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [http://www.cs.ox.ac.uk/conferences/fscd2017/ Second International Conference on Formal Structures for Computation and Deduction (FSCD)] and it will take place "live" during the conference. The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: July 31, 2017 (detail: [[Termination_Competition_2017_Registration]])<br />
* Problem Submission: August 14, 2017 <br />
* Updates of Registered Tools: August 21, 2017 <br />
* Competition: September 5-6, 2017<br />
<br />
== Results == <br />
<br />
* competition https://termcomp.imn.htwk-leipzig.de/competitions/Y2017<br />
* demonstration https://termcomp.imn.htwk-leipzig.de/competitions/67<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
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 FSCD 2017. <br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Akihisa Yamada, NII, Japan<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)<br />
* Akihisa Yamada, NII, Japan (CPF and TPDB)<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2017 Registration]]<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
this refers to StarExec in general, and not to Termination in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [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])<br />
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to akihisa.yamada<at>uibk.ac.at<br />
<br />
== Changes with respect to 2016 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
* New category proposal: Certified [[Transition Systems|ITS]] Termination<br />
<!--<br />
Adopted changes: --><br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2017&diff=1775Termination Competition 20172018-04-10T07:35:35Z<p>Giesl: added Christian and updated Akihisa's affiliation</p>
<hr />
<div>In 2017, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [http://www.cs.ox.ac.uk/conferences/fscd2017/ Second International Conference on Formal Structures for Computation and Deduction (FSCD)] and it will take place "live" during the conference. The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: July 31, 2017 (detail: [[Termination_Competition_2017_Registration]])<br />
* Problem Submission: August 14, 2017 <br />
* Updates of Registered Tools: August 21, 2017 <br />
* Competition: September 5-6, 2017<br />
<br />
== Results == <br />
<br />
* competition https://termcomp.imn.htwk-leipzig.de/competitions/Y2017<br />
* demonstration https://termcomp.imn.htwk-leipzig.de/competitions/67<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
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 FSCD 2017. <br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Christian Sternagel, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Akihisa Yamada, NII, Japan<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)<br />
* Akihisa Yamada, NII, Japan (CPF and TPDB)<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2017 Registration]]<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
this refers to StarExec in general, and not to Termination in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [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])<br />
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to akihisa.yamada<at>uibk.ac.at<br />
<br />
== Changes with respect to 2016 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
* New category proposal: Certified [[Transition Systems|ITS]] Termination<br />
<!--<br />
Adopted changes: --><br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=User_talk:Christoph_Walther&diff=1757User talk:Christoph Walther2017-08-07T21:09:47Z<p>Giesl: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:Giesl|Giesl]] ([[User talk:Giesl|talk]]) 23:09, 7 August 2017 (CEST)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2017&diff=1748Termination Competition 20172017-07-17T11:20:22Z<p>Giesl: removed Fred from the SC and changed one occurrence of 2016 to 2017</p>
<hr />
<div>In 2017, the Termination and Complexity Competition <!-- ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation]) --> will be affiliated with the [http://www.cs.ox.ac.uk/conferences/fscd2017/ Second International Conference on Formal Structures for Computation and Deduction (FSCD)] and it will take place "live" during the conference. The competition will be run on the [http://www.starexec.org/ StarExec platform].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: July 31, 2017 (detail: [[Termination_Competition_2017_Registration]])<br />
* Problem Submission: August 14, 2017 <br />
* Updates of Registered Tools: August 21, 2017 <br />
* Competition: September 5-6, 2017 (live data and results: [[Termination_Competition_2017_Data]])<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
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 FSCD 2017. <br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Akihisa Yamada, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)<br />
* Akihisa Yamada, Universität Innsbruck, Austria (CPF and TPDB)<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the competition's organizer, J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2017 Registration]]<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
== StarExec Information ==<br />
<br />
this refers to StarExec in general, and not to Termination in particular.<br />
<br />
* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]<br />
* [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])<br />
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to akihisa.yamada<at>uibk.ac.at<br />
<br />
== Changes with respect to 2016 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
<!--<br />
Adopted changes: --><br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2016 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_and_Complexity_Competition_2016&diff=1655Termination and Complexity Competition 20162016-07-09T12:28:47Z<p>Giesl: /* Competition Procedure */</p>
<hr />
<div>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].<br />
<br />
== Dates ==<br />
<br />
* Tool Registration: July 31, 2016 <br />
* Problem Submission: August 14, 2016 <br />
* Updates of Registered Tools: August 21, 2016 <br />
* Competition: September 5-6, 2016<br />
<br />
== Competition Categories ==<br />
<br />
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, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
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. <br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
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.<br />
<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.<br />
<!-- 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). --><br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* René Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany (StarExec)<br />
* René Thiemann, Universität Innsbruck, Austria (TPDB and CPF)<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the J. Waldmann (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2016 Registration]]<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
== StarExec Wiki ==<br />
<br />
Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
Send new problems for the competition to rene.thiemann<at>uibk.ac.at<br />
<br />
== Changes with respect to 2015 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
<!--<br />
Proposed changes: --><br />
<br />
Adopted changes:<br />
<br />
* 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.<br />
<br />
<br />
<!--<br />
== TODO ==<br />
<br />
See [[Termination Competition 2015 TODO]]<br />
--></div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=User_talk:Akihisa_Yamada&diff=1591User talk:Akihisa Yamada2015-07-23T09:08:13Z<p>Giesl: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:Giesl|Giesl]] ([[User talk:Giesl|talk]]) 11:08, 23 July 2015 (CEST)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=User_talk:Sabel&diff=1546User talk:Sabel2015-06-30T21:51:50Z<p>Giesl: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:Giesl|Giesl]] ([[User talk:Giesl|talk]]) 23:51, 30 June 2015 (CEST)</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2015&diff=1545Termination Competition 20152015-06-29T08:57:58Z<p>Giesl: </p>
<hr />
<div>In 2015, the Termination Competition ([http://lists.lri.fr/pipermail/termtools/2015-June/000984.html Call for Participation])<br />
will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/ CADE-25].<br />
<br />
== Dates ==<br />
<br />
preliminary:<br />
* registration of tools: July 1<br />
* submission of problems: July 7<br />
* updates of registered tools: July 15<br />
<br />
fixed:<br />
* competition runs: August 5 and 6 (during CADE)<br />
<br />
== Competition Categories and Awards ==<br />
<br />
The competition contains several categories from the areas of<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
== Competition Procedure ==<br />
<br />
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]]<br />
There might be modifications of the rules suggested by the organizer and decided by the SC.<br />
<br />
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).<br />
<br />
The tools will be started in their directory and obtain<br />
<br />
* the problem file name on the command line,<br />
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]<br />
<br />
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.<br />
<br />
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). <br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Rene Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
== Registration ==<br />
<br />
Participants must register<br />
<br />
* 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]<br />
<br />
* *and* with the Termination Competition Organizer (so I known what solver/configuration to use). Details will be announced here: [[Termination Competition 2015 Registration]]<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
== StarExec Wiki ==<br />
<br />
Lots of useful information about StarExec is available [https://wiki.uiowa.edu/display/stardev/User+Guide here].<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.<br />
<br />
Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
<br />
The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de<br />
<br />
<br />
== Changes with respect to 2014 ==<br />
<br />
These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding. <br />
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,<br />
or create a new wiki page and put a link here.<br />
<br />
Proposed changes:<br />
<br />
* The answering scheme and the scoring of the complexity category slightly changed. The new version of the grammar and the updated scoring mechanism are described in more detail on the [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity related page], and below is just a small summary of the changes.<br />
** The grammar for answers was simplified and is now less ambiguous.<br />
** The grammar for answers now explicitly contains lower bounds.<br />
** Lower bounds will be counted for complexity.<br />
<br />
Adopted changes:<br />
<br />
* The CPF version has been updated from version 2.2 to version 2.3. This transition consists of purely incremental changes. The details of the changes are documented in the [http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF CPF repository log].<br />
<br />
* In addition to the category for "full" C programs, we also intend to have a category for "C integer" programs. These are essentially integer transition systems formulated as imperative programs in C syntax. A detailed definition can be found [http://www.termination-portal.org/wiki/C_Integer_Programs here].</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014_Questionnaire&diff=1517Termination Competition 2014 Questionnaire2014-07-31T17:07:53Z<p>Giesl: /* 5. What were the most positive aspects of your experience running your competition on StarExec? */</p>
<hr />
<div>The following questions regarding Star-Exec are being asked by Aaron Stump and Cesare Tinelli,<br />
to all Summer 2014 competition organizers. I (J.W.) will answer, by August 5, and I'd like to collect your comments here.<br />
Just enter below the question, but keep the question intact. (I am dropping some administrative questions, but keep the original numbering.)<br />
<br />
== 4. What were the advantages and disadvantages of using StarExec for you as competition organizer, in comparison with whatever alternative you would have utilized instead of StarExec? ==<br />
<br />
== 5. What were the most positive aspects of your experience running your competition on StarExec? ==<br />
<br />
It is not longer necessary to maintain hardware and software for each competition separately. This makes the competition more independent of individual research groups and their funding.<br />
<br />
The computing power allowed us to run the competition in much less time than before.<br />
<br />
== 6. What were the negative aspects? ==<br />
<br />
It was not (easily) possible to install auxiliary software needed by the tools.<br />
<br />
It was not possible to access remote machines from StarExec, which is needed for some commercial tools that are not willing to let their binaries run on StarExec itself.<br />
<br />
== 10. Where do you think we should focus our development efforts going forward? ==<br />
A few of the things we are considering are: additional interfaces for viewing job results (maybe similar to the 2-dimensional grid used in Termination; other suggestions?), solver pipelines (output from one stage becomes benchmark for input to the next stage; other details to be determined), more work to make it possible to install and run StarExec on your own server or computer (abstract out security-critical details, installation documention, and abstract the interface to GridEngine so you can use a different third-party tool to run jobs on a cluster, or even just your own desktop), commitment to and documentation of the URLs used for communicating directly with the server. <br />
<br />
== 11. Do you expect you or your colleagues will likely want to run the next edition of your competition on StarExec? ==<br />
<br />
== 12. How adequate was the help you were able to get either directly from the StarExec team or from the forum? ==<br />
<br />
== 13. How satisfied do you perceive the participants in your competition were with their experience using StarExec? ==<br />
<br />
== 14. Were there any recurring issues or complaints from the participants in your competition? ==<br />
<br />
== 15. Any further comments or suggestions? ==</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014_Questionnaire&diff=1516Termination Competition 2014 Questionnaire2014-07-31T17:06:46Z<p>Giesl: /* 6. What were the negative aspects? */</p>
<hr />
<div>The following questions regarding Star-Exec are being asked by Aaron Stump and Cesare Tinelli,<br />
to all Summer 2014 competition organizers. I (J.W.) will answer, by August 5, and I'd like to collect your comments here.<br />
Just enter below the question, but keep the question intact. (I am dropping some administrative questions, but keep the original numbering.)<br />
<br />
== 4. What were the advantages and disadvantages of using StarExec for you as competition organizer, in comparison with whatever alternative you would have utilized instead of StarExec? ==<br />
<br />
== 5. What were the most positive aspects of your experience running your competition on StarExec? ==<br />
<br />
== 6. What were the negative aspects? ==<br />
<br />
It was not (easily) possible to install auxiliary software needed by the tools.<br />
<br />
It was not possible to access remote machines from StarExec, which is needed for some commercial tools that are not willing to let their binaries run on StarExec itself.<br />
<br />
== 10. Where do you think we should focus our development efforts going forward? ==<br />
A few of the things we are considering are: additional interfaces for viewing job results (maybe similar to the 2-dimensional grid used in Termination; other suggestions?), solver pipelines (output from one stage becomes benchmark for input to the next stage; other details to be determined), more work to make it possible to install and run StarExec on your own server or computer (abstract out security-critical details, installation documention, and abstract the interface to GridEngine so you can use a different third-party tool to run jobs on a cluster, or even just your own desktop), commitment to and documentation of the URLs used for communicating directly with the server. <br />
<br />
== 11. Do you expect you or your colleagues will likely want to run the next edition of your competition on StarExec? ==<br />
<br />
== 12. How adequate was the help you were able to get either directly from the StarExec team or from the forum? ==<br />
<br />
== 13. How satisfied do you perceive the participants in your competition were with their experience using StarExec? ==<br />
<br />
== 14. Were there any recurring issues or complaints from the participants in your competition? ==<br />
<br />
== 15. Any further comments or suggestions? ==</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Integer_Term_Rewriting&diff=1487Integer Term Rewriting2014-06-17T16:00:29Z<p>Giesl: </p>
<hr />
<div>The main idea of ITRSs is to add<br />
pre-defined constructors for integers (the integers themselves) and Booleans<br />
(true / false) and arithmetic, relational and Boolean functions like <br />
<br />
+, -, *,/ ,%, >, >=, <, &&, ||, !, ... <br />
<br />
to conventional TRSs using the ''innermost'' rewrite strategy. To this<br />
aim it is necessary to extend the XTC format by the ability to represent<br />
pre-defined semantics for function symbols.<br />
Not only ITRSs, but also other extensions with pre-defined functions can be<br />
represented using this extension of the XTC format. A formal definition of ITRSs and their evaluation can be found <br />
in [http://verify.rwth-aachen.de/giesl/papers/idp-distribute.pdf this paper].<br />
<br />
[http://lists.lri.fr/pipermail/termtools/2009-October/000775.html full text of the proposal]<br />
<br />
[[Category:Categories]]</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Integer_Term_Rewriting&diff=1486Integer Term Rewriting2014-06-17T15:58:44Z<p>Giesl: </p>
<hr />
<div>The main idea of ITRSs is to add<br />
pre-defined constructors for integers (the integers themselves) and Booleans<br />
(true / false) and arithmetic, relational and Boolean functions like <br />
<br />
+, -, *,/ ,%, >, >=, <, &&, ||, !, ... <br />
<br />
to conventional TRSs using the ''innermost'' rewrite strategy. To this<br />
aim it is necessary to extend the XTC format by the ability to represent<br />
pre-defined semantics for function symbols.<br />
Not only ITRSs, but also other extensions with pre-defined functions can be<br />
represented using this extension of the XTC format.<br />
<br />
[http://lists.lri.fr/pipermail/termtools/2009-October/000775.html full text of the proposal]<br />
<br />
[[Category:Categories]]</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014&diff=1437Termination Competition 20142014-05-26T11:59:06Z<p>Giesl: /* Competition Categories and Awards */</p>
<hr />
<div>In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].<br />
<br />
== Dates (tentative) ==<br />
<br />
* call for tools, certifiers, problems: May 26<br />
* registration of tools: June 15<br />
* updates of registered tools, submission of problems: July 1<br />
* competition runs: July 15 - 20<br />
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.<br />
<br />
== Competition Categories and Awards ==<br />
<br />
The competition contains several categories, grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant would produce a zero score.) <br />
A category is only run at the competition if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base.<br />
<br />
== New Categories ==<br />
<br />
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]).<br />
<br />
Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.<br />
<br />
== Competition Procedure ==<br />
<br />
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.<br />
<br />
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).<br />
<br />
For nearly all categories, the tools will be started in their directory and obtain two parameters: <br />
<br />
* the problem file and <br />
* the timeout in seconds. <br />
<br />
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.<br />
<br />
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). <br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Rene Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Stefan von der Krone, HTWK Leipzig, Germany<br />
<br />
== Registration Info (tentative) ==<br />
<br />
Participants must register on [http://www.starexec.org StarExec], and send an email to the organizers, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
The competition organizers can be reached at termcomp<at>htwk-leipzig.de</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014&diff=1436Termination Competition 20142014-05-26T11:58:31Z<p>Giesl: /* Competition Procedure */</p>
<hr />
<div>In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].<br />
<br />
== Dates (tentative) ==<br />
<br />
* call for tools, certifiers, problems: May 26<br />
* registration of tools: June 15<br />
* updates of registered tools, submission of problems: July 1<br />
* competition runs: July 15 - 20<br />
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.<br />
<br />
== Competition Categories and Awards ==<br />
<br />
The competition contains several categories, grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant will produce a zero score.)<br />
<br />
== New Categories ==<br />
<br />
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]).<br />
<br />
Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.<br />
<br />
== Competition Procedure ==<br />
<br />
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.<br />
<br />
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).<br />
<br />
For nearly all categories, the tools will be started in their directory and obtain two parameters: <br />
<br />
* the problem file and <br />
* the timeout in seconds. <br />
<br />
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.<br />
<br />
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). <br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Rene Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Stefan von der Krone, HTWK Leipzig, Germany<br />
<br />
== Registration Info (tentative) ==<br />
<br />
Participants must register on [http://www.starexec.org StarExec], and send an email to the organizers, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
The competition organizers can be reached at termcomp<at>htwk-leipzig.de</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014&diff=1435Termination Competition 20142014-05-26T11:58:07Z<p>Giesl: /* Competition Procedure */</p>
<hr />
<div>In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].<br />
<br />
== Dates (tentative) ==<br />
<br />
* call for tools, certifiers, problems: May 26<br />
* registration of tools: June 15<br />
* updates of registered tools, submission of problems: July 1<br />
* competition runs: July 15 - 20<br />
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.<br />
<br />
== Competition Categories and Awards ==<br />
<br />
The competition contains several categories, grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant will produce a zero score.)<br />
<br />
== New Categories ==<br />
<br />
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]).<br />
<br />
Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.<br />
<br />
== Competition Procedure ==<br />
<br />
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. A category is only run if there are at least 2 participants and at least 40 examples <br />
for this category in the underlying termination problem data base. 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.<br />
<br />
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).<br />
<br />
For nearly all categories, the tools will be started in their directory and obtain two parameters: <br />
<br />
* the problem file and <br />
* the timeout in seconds. <br />
<br />
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.<br />
<br />
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). <br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Rene Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Stefan von der Krone, HTWK Leipzig, Germany<br />
<br />
== Registration Info (tentative) ==<br />
<br />
Participants must register on [http://www.starexec.org StarExec], and send an email to the organizers, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
The competition organizers can be reached at termcomp<at>htwk-leipzig.de</div>Gieslhttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2014&diff=1434Termination Competition 20142014-05-26T11:32:47Z<p>Giesl: /* Registration info (tentative) */</p>
<hr />
<div>In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].<br />
<br />
== Dates (tentative) ==<br />
<br />
* call for tools, certifiers, problems: May 26<br />
* registration of tools: June 15<br />
* updates of registered tools, submission of problems: July 1<br />
* competition runs: July 15 - 20<br />
* results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.<br />
<br />
== Competition Categories and Awards ==<br />
<br />
The competition contains several categories, grouped in three meta-categories:<br />
<br />
* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)<br />
* complexity analysis of term rewriting (all complexity categories)<br />
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)<br />
<br />
In each meta-category, a medal will be awarded to the highest-scoring solver.<br />
<br />
For every meta-category, we consider the sum of the scores for each category within that meta-category:<br />
The score of a tool is determined by the number of other tools which could be beaten in that category.<br />
<br />
This puts the emphasis on categories with many competitors.<br />
(In particular, a category with just one entrant will produce a zero score.)<br />
<br />
== New Categories ==<br />
<br />
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]).<br />
<br />
Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.<br />
<br />
== Competition Procedure ==<br />
<br />
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.<br />
<br />
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).<br />
<br />
For nearly all categories, the tools will be started in their directory and obtain two parameters: <br />
<br />
* the problem file and <br />
* the timeout in seconds. <br />
<br />
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.<br />
<br />
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). <br />
<br />
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).<br />
<br />
== Committees ==<br />
<br />
Steering Committee<br />
* Jürgen Giesl, RWTH Aachen, Germany<br />
* Frederic Mesnard, Université de la Réunion, France<br />
* Albert Rubio (chair), UPC Barcelona, Spain<br />
* Rene Thiemann, Universität Innsbruck, Austria<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
<br />
Organizing Commmittee<br />
* Johannes Waldmann, HTWK Leipzig, Germany<br />
* Stefan von der Krone, HTWK Leipzig, Germany<br />
<br />
== Registration Info (tentative) ==<br />
<br />
Participants must register on [http://www.starexec.org StarExec], and send an email to the organizers, indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].<br />
<br />
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.<br />
<br />
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.<br />
<br />
== Technical Detail ==<br />
<br />
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.<br />
<br />
Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].<br />
<br />
== Contact ==<br />
<br />
To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de. <br />
The competition organizers can be reached at termcomp<at>htwk-leipzig.de</div>Giesl