Termination-Portal.org - User contributions [en]

Termination Competition 2025

2025-07-04T13:31:12Z

Fuhs: Dates for TermComp 2025, taken from https://lists.rwth-aachen.de/archives/list/termtools@lists.rwth-aachen.de/thread/FAA6ENEMMX5ANNGUOLXRKGCMFFJ7PV37/

The Termination and Complexity Competition (termCOMP) 2025 will be affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
The first run will be shortly before WST, followed by a bug/conflict reporting phase and allowance for bug fixes.
The final run and a presentation of the final results will be live at WST.



== Dates ==

* Tool and Benchmark Submission: August 6, 2025
* First Run: August 20, 2025
* Bugfix Deadline: August 27, 2025
* Final Run: September 3/4, 2025
* Presentation of the results at WST: September 4, 2025


== Competition Categories ==

The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...)

Proposals for new categories are welcome.

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

== Competition Procedure ==

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

The wall-clock timeout will be 60 seconds. Further technical information is available [[Termination Competition 2025 technical details|here]].


The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.
The SC will decide what should be penalized, depending on the discussion among the participants.

== Steering Committee ==

* Florian Frohn (Chair and Organizer), RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Étienne Payet, Université de La Réunion
* Akihisa Yamada, AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository] (for rewriting and integer transition systems) or the [https://github.com/TermCOMP/TPDB TPDB repository] (for programming languages).

We recommend to register early, and update information as needed.

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== Technical Details ==

Competition data will be presented via [https://github.com/TermCOMP/starexec-master starexec-master]
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).

Technical details about the execution platform are available [[Termination Competition 2025 technical details|here]].

== Contact ==

Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de

To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.

== Changes with respect to 2024 ==

These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding.
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,
or create a new wiki page and put a link here.

Adopted changes:

* We will use the new ARI format for all Integer Transition System categories, see [https://termination-portal.org/wiki/Term_Rewriting#Integer_Transition_Systems here] for details and [https://github.com/TermCOMP/its-conversion here] for a converter.

Proposed changes:

* We plan to use CPF 3, see [http://cl-informatik.uibk.ac.at/isafor/cpf3.html here] for details and a converter.
* On the RWTH cluster, our computing time is limited. As it's difficult to predict how much testing will be needed on the new platform before the competition, I (Florian) would like to run the competition with a 60 instead of 300s timeout to avoid running out of credits. If things go well, we can switch back to a 300s timeout in 2026.

Termination Competition

2025-07-04T13:15:32Z

Fuhs: Added upcoming TermComp 2025

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
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.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn. Jobs are run on Star-Exec.

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[Term Rewriting|string and term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[C_Complexity|complexity of C programs]]
* termination of [[Term Rewriting|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[Cycle_Rewriting|termination of cycle rewriting]]
* [[Probabilistic_Rewriting|termination of probabilistic term rewriting]] (since 2024)

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[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].

* [[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]

* [[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]

* [[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]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* 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]

* [[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]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

People:Carsten Fuhs

2023-02-03T17:24:35Z

Fuhs: updated e-mail address and role

{{Person
|firstname=Carsten
|middlenames=
|lastname=Fuhs
|titles=
|email=c.fuhs@bbk.ac.uk
|homepage=http://www.dcs.bbk.ac.uk/~carsten/
|country=United Kingdom
|university=Birkbeck, University of London
|department=Computer Science and Information Systems
|role=Senior Lecturer (Associate Professor) 
}}

WST

2017-11-13T09:22:24Z

Fuhs: WST 2018

The International Workshop on Termination (WST) brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:

* [http://wst2018.webs.upv.es/ 16th International Workshop on Termination] during [http://www.floc2018.org/ Federated Logic Conference (FLoC)], Oxford, United Kingdom, July 18-19, 2018.

Information about previous workshops can be found online:
* [http://cl-informatik.uibk.ac.at/events/wst-2016/ 15th International Workshop on Termination] at [http://cl-informatik.uibk.ac.at/events/cla-2016/ Computational Logic in the Alps], Obergurgl, Austria, September 5-7, 2016.
* [http://vsl2014.at/wst/ 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014
* Joint Workshop on Termination [http://www.imn.htwk-leipzig.de/WST2013/ WST2013] and on Foundational and Practical Aspects of Resource Analysis [http://fopara2013.cs.unibo.it/ FOPARA], Bertinoro, Italy, August 29-31, 2013
* [http://cl-informatik.uibk.ac.at/users/georg/events/wst2012 12th International Workshop on Termination, Obergurgl, February 19-23, 2012]
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

User talk:Epayet

2017-08-20T12:27:44Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!'''
We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]].
Again, welcome and have fun! [[User:Fuhs|Fuhs]] ([[User talk:Fuhs|talk]]) 14:27, 20 August 2017 (CEST)

Termination Competition

2015-07-10T22:23:36Z

Fuhs: /* Annual International Termination Competition */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
In 2014, we moved to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2015|Termination Competition 2015]] will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/home CADE].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[termination of integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)

Planned extensions for 2015:

* [[C_Integer_Programs|termination of C integer programs]]
* [[Cycle_Rewriting|termination of cycle rewriting]]

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* 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]

* [[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]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition

2015-07-10T22:21:43Z

Fuhs: update categories for TermComp 2015

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marche, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by Rene Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
In 2014, we moved to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2015|Termination Competition 2015]] will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/home CADE].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[termination of integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)

Planned extensions for 2015:

* [[C_Integer_Programs|termination of C integer programs]]
* [[Cycle_Rewriting|termination of cycle rewriting]]

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* 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]

* [[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]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition

2015-07-10T22:14:42Z

Fuhs: link to wiki page for C programs

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marche, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by Rene Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
In 2014, we moved to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2015|Termination Competition 2015]] will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/home CADE].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[C_Programs|termination of C programs]] (since 2014)
* [[termination of integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* 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]

* [[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]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition

2015-07-10T22:12:35Z

Fuhs: record TermComp state of 2014

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marche, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by Rene Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
In 2014, we moved to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2015|Termination Competition 2015]] will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/home CADE].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
* [[termination of C programs]] (since 2014)
* [[termination of integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* 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]

* [[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]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

People:Carsten Fuhs

2015-07-10T22:02:49Z

Fuhs: now lecturer at Birkbeck

{{Person
|firstname=Carsten
|middlenames=
|lastname=Fuhs
|titles=
|email=carsten@dcs.bbk.ac.uk
|homepage=http://www.dcs.bbk.ac.uk/~carsten/
|country=United Kingdom
|university=Birkbeck, University of London
|department=Computer Science and Information Systems
|role=Lecturer (Assistant Professor) 
}}

Bibtex:AProVE14

2014-07-29T07:55:44Z

Fuhs: Updated bibtex for AProVE System Description

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>

@inproceedings{AProVE14,
author = {Giesl, J\"urgen and
Brockschmidt, Marc and
Emmes, Fabian and
Frohn, Florian and
Fuhs, Carsten and
Otto, Carsten and
Pl\"ucker, Martin and
Schneider-Kamp, Peter and
Str\"oder, Thomas and
Swiderski, Stephanie and
Thiemann, Ren\'e},
title = "Proving Termination of Programs Automatically with \textsf{AProVE}",
booktitle = "Proceedings IJCAR '14",
year = {2014},
series = {LNAI},
volume = {8562},
pages = {184-191},
publisher = {Springer},
}

</bibtex>

Tools:AProVE

2014-05-25T20:25:55Z

Fuhs: reference current system description for AProVE at IJCAR 2014

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=[[People:Jürgen Giesl|Jürgen Giesl]], [[People:René Thiemann|René Thiemann]], [[People:Peter Schneider-Kamp|Peter Schneider-Kamp]], [[People:Stephan Swiderski|Stephan Swiderski]], [[People:Carsten Fuhs|Carsten Fuhs]], [[People:Carsten Otto|Carsten Otto]], [[People:Fabian Emmes|Fabian Emmes]] et al.
|publication=[[Bibtex:AProVE14|Proving Termination of Programs Automatically with AProVE]]
}}

Bibtex:AProVE14

2014-05-25T20:22:34Z

Fuhs: /* BibTex */

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>

@inproceedings{AProVE14,
author = {Giesl, J\"urgen and
Brockschmidt, Marc and
Emmes, Fabian and
Frohn, Florian and
Fuhs, Carsten and
Otto, Carsten and
Pl\"ucker, Martin and
Schneider-Kamp, Peter and
Str\"oder, Thomas and
Swiderski, Stephanie and
Thiemann, Ren\'e},
title = "Proving Termination of Programs Automatically with \textsf{AProVE}",
booktitle = "Proceedings IJCAR '14",
year = {2014},
series = {LNAI},
note = {To appear.},
publisher = {Springer},
}

</bibtex>

Bibtex:AProVE14

2014-05-25T20:17:40Z

Fuhs: reference to current system description for AProVE

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>

@inproceedings{AProVE14,
author = {Giesl, J\"urgen and
Brockschmidt, Marc and
Emmes, Fabian and
Frohn, Florian and
Fuhs, Carsten and
Otto, Carsten and
Pl\"ucker, Martin and
Schneider-Kamp, Peter and
Str\"oder, Thomas and
Swiderski, Stephanie and
Thiemann, Ren\'e},
title = "Proving Termination of Programs Automatically with \textsf{AProVE}",
booktitle = "Proc.\ IJCAR~'14",
year = {2014},
series = {LNAI},
note = {To appear.},
publisher = {Springer},
}

</bibtex>

TPDB

2014-03-07T11:19:29Z

Fuhs: TPDB 8.0.6 was already available in 2012, see also http://termcomp.uibk.ac.at/2012/rules.html

The Termination Problems Data Base collects termination problems
that are being used in termination competitions.

== Syntax and semantics specification ==

* for versions from 7.* onwards (XML format): http://termcomp.uibk.ac.at/tpdb/xtc.xsd
* for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html

see also:

* output specification for certified categories: http://cl-informatik.uibk.ac.at/software/cpf/

== Data ==
* 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/
* version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz
* version 5.0.2 (2008..2009) http://termcomp.uibk.ac.at/termcomp/docs/tpdb-5.0.2.tar.gz
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/

== Sources ==

The following are references for classical problem sets that appear in TPDB.

* TRS/SK90 Joachim Steinbach, Ulrich Kühler: Check your Ordering - termination proofs and open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990.
* 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
* 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
* SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?)

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.

== Tools ==
* converter from pre-7 (textual) format to 7.* (XML) format: http://termcomp.uibk.ac.at/status/convert.jar , usage:

java -jar convert.jar someTrs.trs > someTrs.xml

* converter from 7.* (XML) format to pre-7 (textual) format: http://termcomp.uibk.ac.at/status/xtc2tpdb.xsl , usage:

xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs

* Haskell library for reading and writing TPDB (plain and XML format) [http://hackage.haskell.org/package/tpdb]

User talk:Ffrohn

2014-03-04T14:18:58Z

Fuhs: Welcome!

WST

2014-02-28T16:50:10Z

Fuhs: link to WST 2014, dates, location

The International Workshop on Termination (WST) brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [http://vsl2014.at/wst/ 14th International Workshop on Termination] during [http://vsl2014.at/ Vienna Summer of Logic], Vienna, Austria, July 17-18, 2014

Information about previous workshops can be found online:
* Joint Workshop on Termination [http://www.imn.htwk-leipzig.de/WST2013/ WST2013] and on Foundational and Practical Aspects of Resource Analysis [http://fopara2013.cs.unibo.it/ FOPARA], Bertinoro, Italy, August 29-31, 2013
* [http://cl-informatik.uibk.ac.at/users/georg/events/wst2012 12th International Workshop on Termination, Obergurgl, February 19-23, 2012]
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

People:Carsten Fuhs

2013-09-08T12:08:21Z

Fuhs: postdoc

{{Person
|firstname=Carsten
|middlenames=
|lastname=Fuhs
|titles=
|email=c.fuhs@cs.ucl.ac.uk
|homepage=http://www.cs.ucl.ac.uk/staff/C.Fuhs/
|country=United Kingdom
|university=University College London
|department=Computer Science
|role=Post-Doctoral Research Assistant 
}}

Termination Competition 2012 Comments

2012-06-28T12:16:02Z

Fuhs: verb tense

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain. ((July 27, 10:48)
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (111) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop). (July 27, 10:48)

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Java Bytecode =
* The example "Overflow.jar" was chosen. However, its termination depends on the handling of integers. If integers are implemented like in Java (i.e. their range is bounded), this example does not terminate (for any input). Maybe we should remove this (and other examples whose termination behaviour depends on the implementation of bounded integers)?

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ_10/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof. CF As far as I recall, AProVE generated a proof of this size for this example already in the competition of 2010. For obvious reasons, I do not dare to check this on TermComp right now.

Termination Competition 2012 Comments

2012-06-28T12:14:34Z

Fuhs: Huge proofs generated already in 2010

Participants and observers may put their comments here. These could be used when a report on the competition is prepared.

= SRS Certified =

* machbox-cert gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=402459&cid=39568 here]. What happened? It prints YES on stdout, but then CPF output raises an exception because a pattern for RIsEmpty is missing [http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=tpdb.git;a=blob;f=TPDB/CPF/Proof/Xml.hs;h=8cd244666cc1b7f7ea8dc435534f74130ae7bd3f;hb=HEAD#l85 here]. Obviously the author did not believe that any of the problems could be solved by linear additive weights alone ...
* matchbox-cert currently has a higher score than matchbox-uncert which is interesting. Johannes, can you please explain. ((July 27, 10:48)
* AProVE-CeTA gets a "failed validation" [http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=404090&cid=108046 here]. The reason is that AProVE used some additional inference rules that are not described in their IJCAR'12 paper on non-looping non-terminating derivations.
* currently, AProVE and AProVE-CeTA have the same YES-count (111) which shows that the restriction to certifiable techniques imposes a neglectable restriction for SRSs. For NO-answers, AProVE beats AProVE-Cert due to the use of an uncertified technique to find non-looping non-terminating derivations of Oppelt08 (which however in several examples just detected a loop). (July 27, 10:48)

= Complexity Certified =

This year, for the first time, complexity proofs can also be provided in the standardized CPF format which allows for certification. Here, TcT-Cert ant CaT-Cert and restricted versions of TcT and CaT which only use techniques that are currently supported by CeTA, i.e.: rule-shifting using matrix-interpretations over the naturals or the rationals. Clearly, this is a severe restriction in the configuration of the tools. The consequences are however not always severe:
* For '''Derivational Complexity - Full Rewriting''', the certified tools already achieve over 60 % of the score of the uncertified tools. Some examples could not be handled at all (the main missing techniques seems to be matchbounds) and for some TRSs the derived complexity is just higher (currently CeTA can only infer the dimension of a triangular matrix interpretation as degree of the complexity.)
* For '''Derivational Complexity - Innermost''', the difference in score is much higher: the certified tool got around 35 % of the uncertified tool. This is explained easily since one additional missing technique is often applied on these examples: the removal of useless rules, i.e., rules which are never applicable since some argument of the left-hand side contains already a redex (which in my opinion (RT) shows that these examples are not really intended for innermost rewriting).
* For '''Runtime Complexity''' the certifiers clearly miss Dependency Pairs and related techniques and here the difference in score is highest: the certified tool got only 28 % for full rewriting and 21 % for innermost rewriting of the score in comparison to the uncertified tools.
* Although the uncertified tools should be more powerful, one can also find some examples where only the certified tools have been successful. The obvious reason is that if less techniques are available then more time can be spent on each individual technique, i.e., search for suitable orders, and sometimes this additional time was required to find the proof.

= TRS and TRS innermost Certified =
* The main difference between AProVE and AProVE-CeTA is due to three techniques: bounded increase, the induction processor, and uncurrying/A-transformation in the innermost case.

= Java Bytecode =
* The example "Overflow.jar" was chosen. However, its termination depends on the handling of integers. If integers are implemented like in Java (i.e. their range is bounded), this example does not terminate (for any input). Maybe we should remove this (and other examples whose termination behaviour depends on the implementation of bounded integers)?

= Termcomp =
* AProVE has hit a new record in large proofs: the one for TRS/MNZ_10/labelled is 535 MB large. Please do not try to load it during the competition, as most likely it will result in an out-of-memory exception on the termcomp-platform when trying to generate the HTML-page presenting this proof. CF As far as I recall, AProVE has generated a proof of this size for this example already in the competition of 2010. For obvious reasons, I do not dare to check this on TermComp right now.

People:Carsten Fuhs

2012-03-06T20:38:55Z

Fuhs: C. Fuhs has moved to University College London

{{Person
|firstname=Carsten
|middlenames=
|lastname=Fuhs
|titles=
|email=c.fuhs@cs.ucl.ac.uk
|homepage=http://www.cs.ucl.ac.uk/staff/C.Fuhs/
|country=United Kingdom
|university=University College London
|department=Computer Science
|role=Research Assistant 
}}

User talk:Hezzel

2011-11-07T21:37:44Z

Fuhs: Welcome!

Termination Portal

2011-09-21T19:40:02Z

Fuhs: Grammar

Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).

This portal aims to provide the research community with up-to-date information about the field
of termination analysis.
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),
[[:Category:News|News]] (information about events and new publications),
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and
[[:Category:Bibtex|References]] (publications related to termination analysis).
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].

Have [[Suggestions]] to improve this web resource?
- How to [[Contribute]].

=Recent News=
<dpl>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</dpl>
Older news entries can be found on the [[:Category:News|news page]].

Termination Competition

2011-05-11T20:05:07Z

Fuhs: Higher order termination joined the competition in 2010

TPDB

2011-02-15T00:13:17Z

Fuhs: mention version 8.* of TPDB

User talk:Schernhammer

2009-12-30T10:21:14Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 10:21, 30 December 2009 (UTC)

Tools:Rainbow

2009-10-27T17:34:50Z

Fuhs: Updated homepage (http://color.loria.fr has been a deadlink for a while now)

{{Tool
|shortname=Rainbow
|longname=Termination proof certifier
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=Frederic Blanqui and Adam Koprowski
|publication=
}}

TPDB

2009-05-13T21:42:17Z

Fuhs: Version 5 was also used in the competition of Nov 2008

The Termination Problems Data Base collects termination problems
that are being used in termination competitions.

Syntax and semantics specification:
* for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html

Data:
* version 5.* (2008 .. 2009) http://dev.aspsimon.org/projects/termcomp/downloads/
* earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/

Tools:AProVE

2009-05-13T20:59:54Z

Fuhs: set reference to the more recent IJCAR'06 paper

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=[[People:Jürgen Giesl|Jürgen Giesl]], [[People:René Thiemann|René Thiemann]], [[People:Peter Schneider-Kamp|Peter Schneider-Kamp]], [[People:Stephan Swiderski|Stephan Swiderski]], [[People:Carsten Fuhs|Carsten Fuhs]], [[People:Carsten Otto|Carsten Otto]], [[People:Fabian Emmes|Fabian Emmes]] et al.
|publication=[[Bibtex:GST06|AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework]]
}}

Bibtex:GST06

2009-05-13T20:55:52Z

Fuhs: added IJCAR'06 paper on AProVE

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@inproceedings{IJCAR06,
author = "J. Giesl and P. Schneider-Kamp and R. Thiemann",
title = "AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework",
booktitle = "Proceedings IJCAR '06",
publisher = "Springer",
series = "LNAI 4130",
pages = "281-286",
year = "2006"
}

</bibtex>

Tools:AProVE

2009-05-13T20:50:18Z

Fuhs: added developer Fabian Emmes

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=[[People:Jürgen Giesl|Jürgen Giesl]], [[People:René Thiemann|René Thiemann]], [[People:Peter Schneider-Kamp|Peter Schneider-Kamp]], [[People:Stephan Swiderski|Stephan Swiderski]], [[People:Carsten Fuhs|Carsten Fuhs]], [[People:Carsten Otto|Carsten Otto]], [[People:Fabian Emmes|Fabian Emmes]] et al.
|publication=[[Bibtex:Giesl04|Automated Termination Proofs with AProVE]]
}}

User talk:Nguyen

2009-05-13T13:46:13Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 13:46, 13 May 2009 (UTC)

User talk:UlrichSG

2009-04-24T09:50:09Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 09:50, 24 April 2009 (UTC)

WScT

2008-11-25T21:16:23Z

Fuhs: Update of previous events

== Goals ==

Termination is an important and difficult problem. Many methods and criteria have been developed,
and they are being used in various programs (termination provers),
see for instance the international [[Termination_Competition]] .

These programs are more and more complex and are being applied on larger and larger input systems.
For these tools to be used in the certification of critical systems and proof assistants, their results must be certified.

The Workshops on Certified Termination aim to bring together researchers working in the field
for a discussion of current results, as well as directions of further research and implementation.

== Events ==

Previous events:
* May 17 - 19, 2008 in Leipzig, Germany: [[WScT08]]
* May 11 - 12, 2007 in Nancy, France: [http://color.loria.fr/workshop.html WScT07]

== Resources ==

* [[Tools:CoLoR|the CoLoR project]]

User talk:Pons

2008-07-09T16:02:14Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 16:02, 9 July 2008 (UTC)

WScT08

2008-05-15T18:22:22Z

Fuhs: /* Registration */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel,
** I would like to present:
*** summary of what I presented in Nancy last year + progress report
*** short overview of (ongoing) work on formalizing dependency pairs, subterm criterion, and SCC decomposition in Isabelle
** I would like to discuss:
*** how to encode (estimated) dependency graphs and SCCs in Rainbow

* Adam Koprowski, (topic: TBA)

* René Thiemann, topics (presented in combination with Simon)
** (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community
** (since the TC should not be the main topic of this workshop, I would suggest to schedule these parts on Sunday)

* Simon Bailey, topics:
** the current state of the new implementation of the termination competition.

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Carsten Fuhs

* Raúl Gutiérrez,

* Évelyne Contejean. I and Xavier would like to give a talk on Sunday about the A3Pat approach.

* Xavier Urbain

* Andreas Gebhardt

== Program ==

I think we have two main topics
* A: (future of) certified termination
* B: (certified) termination competition

What's your preference (vote here)
* Saturday: A, Sunday: B
* Saturday: B, Sunday: A
* (X) mixed: Saturday: Introduction, Sunday: Discussion

We should aim for a "results" session on Monday
(write down results of discussion, and open problems).

== Local Organization ==

=== Date/time ===

session times are provisional

* Saturday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
* Sunday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
** Workshop Dinner 7 p.m. at [http://www.da-vito-leipzig.de/anfahrt.htm Ristorante da Vito]
* Monday 9 a.m. -- 1 p.m. , Room Li108

=== Location ===

HTWK, Fachbereich IMN, Gustav-Freytag-Straße 42a, 04275 Leipzig
http://www.htwk-leipzig.de/hochsch/lageplan.pdf
* Z017 in ground floor of Zuse-Bau
* Li108 in first floor of Lipsius-Bau

=== Food ===

* coffee and soda provided at the workshop (small fee)
* lunch Saturday/Sunday: several small restaurants nearby
* lunch Monday: Mensa/Cafeteria HTWK

=== Accomodation ===

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

=== Travel info ===

* from Airport Leipzig/Halle to Leipzig Hauptbahnhof (central station, right next to city center): several trains. Takes 15 min, goes every 30 min
* from Hauptbahnhof to HTWK (workshop location): take tram #10 (direction Lößnig) or #11 (direction Markkleeberg Ost), until station "Connewitz Kreuz"
(takes 15 min, goes every 15 min) then walk (5 min).

=== Tourist info ===

places to go:

* cultural/historic/shopping: city center (tram stations Wilhelm-Leuschner-Platz, Augustusplatz)
* entertainment (cafes, restaurants, clubs, bars): Karl-Liebknecht-Straße (tram: Südplatz), Gottschedstraße (tram: Thomaskirche)
* recreation: Clara-Zetkin-Park, Cospudener See

... and there's more (so you'll have to come back for [[WST09]])

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

User talk:Urbain

2008-05-07T14:47:08Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 14:47, 7 May 2008 (UTC)

User talk:Contejea

2008-05-07T14:45:28Z

Fuhs: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Fuhs|Fuhs]] 14:45, 7 May 2008 (UTC)

WScT08

2008-04-15T13:29:52Z

Fuhs: /* Registration/Program */

= Workshop on Certified Termination WScT08 =

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration/Program ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel, (Topic: TBA)

* Adam Koprowski, (topic: TBA)

* René Thiemann, topics to present (in combination with other colleagues from Innsbruck) and discuss
** presentation of (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Carsten Fuhs, (topic: TBA)

== Local Organization ==

Details will be fixed soon. Vote here! (Just mark with "X")

=== Options for location ===

* external conference facility (e.g. http://www.mediencampus-villa-ida.de/ ,rent would be 150 EUR per day), on-site restaurant/catering (additional cost)

* (XXX) classroom at HTWK (e.g. "Lipsius-Bau" on that map: http://www.htwk-leipzig.de/hochsch/lageplan.pdf , low or no cost) , self-catering (several small restaurants nearby)

=== Options for date/time ===

* workshop start: Saturday
** (XX) morning (9 a.m.) or
** (X) noon (1 p.m.)
* Workshop Dinner (Sunday), booking a table at some restaurant
** in the city center
** (XX) outskirts (may include walk or tram ride)
* workshop end: Monday
** (XX) noon (1 p.m.) or
** afternoon (5 p.m.)

== Accomodation ==

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

Termination Competition

2008-04-09T19:36:21Z

Fuhs: typo

What domain name?

2008-04-07T09:48:09Z

Fuhs: vote

We want to have a domain name for this web site.
What is your preference? Vote here

* termination-portal.org

* termination-portal.info

* termination-live.org (by analogy to satlive.org)

* terminationlive.(org|info) (registrateable via www.verio.com)

* termination.at

or extend the list (but check that the name is free).
(everything like termination.* seems already taken)

Peter: I like termination-portal as it is descriptive. (Carsten Otto thinks the same.)

Carsten Fuhs: Another proposal might be termination.at (still free according to whois). The name is quite catchy and short, and I do not think that using a "national" domain name (here: Austria) would be a big problem. Does anyone know how hard it is to get an .at-domain?

F. Blanqui: I vote for termination-portal.org.

Andreas: I added termination-portal.info and terminationlive.(org|info) but for myself i like terminationlive.org because the analogy to satlive.org and *live* means maybe state of the art ...

C. Fuhs: I would also be fine with termination-portal.org.

Tools:AProVE

2008-03-31T19:20:25Z

Fuhs: added link to Stephan Swiderski

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=[[People:Jürgen Giesl|Jürgen Giesl]], [[People:René Thiemann|René Thiemann]], [[People:Peter Schneider-Kamp|Peter Schneider-Kamp]], [[People:Stephan Swiderski|Stephan Swiderski]], [[People:Carsten Fuhs|Carsten Fuhs]] et al.
}}

People:Stephan Falke

2008-03-31T19:15:20Z

Fuhs: added missing brace

{{Person
|firstname=Stephan
|middlenames=
|lastname=Falke
|titles=
|email=spf@cs.unm.edu
|homepage=http://www.cs.unm.edu/~spf/
|country=USA
|university=University of New Mexico
|department=Computer Science
|role=PhD Student
}}

What domain name?

2008-03-31T13:52:43Z

Fuhs: typo

We want to have a domain name for this web site.
What is your preference? Vote here

* termination-portal.org

* termination-live.org (by analogy to satlive.org)

* termination.at

or extend the list (but check that the name is free).
(everything like termination.* seems already taken)

Peter: I like termination-portal as it is descriptive. (Carsten Otto thinks the same.)

Carsten Fuhs: Another proposal might be termination.at (still free according to whois). The name is quite catchy and short, and I do not think that using a "national" domain name (here: Austria) would be a big problem. Does anyone know how hard it is to get an .at-domain?

What domain name?

2008-03-31T13:09:20Z

Fuhs: added proposal termination.at

Bibtex:FGMSTZ07

2008-03-31T09:09:09Z

Fuhs: SAT'07 paper on SAT solving for finding polynomial interpretations (without and with negative constants)

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==
<bibtex>

@inproceedings{SAT07,
author = {C. Fuhs and J. Giesl and A. Middeldorp and R. Thiemann and P. {Schneider-Kamp} and H. Zankl},
title = {SAT Solving for Termination Analysis with Polynomial Interpretations},
booktitle = {Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007)},
year = {2007},
series = {Lecture Notes in Computer Science},
volume = {4501},
pages = {340-354}
}
</bibtex>

Bibtex:SGST06

2008-03-31T09:04:42Z

Fuhs: L Note/s/ in CS

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==
<bibtex>

@inproceedings{LOPSTR06,
AUTHOR = {P. Schneider-Kamp and J. Giesl and A. Serebrenik and R. Thiemann},
TITLE = {Automated Termination Analysis for Logic Programs by Term Rewriting},
BOOKTITLE = {LOPSTR~'06},
YEAR = {2007},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4407},
PAGES = {177--193},
PUBLISHER = {Springer},
ADDRESS = {Heidelberg}
}
</bibtex>

Bibtex:MORV05

2008-03-31T08:53:46Z

Fuhs: fixed typo in title

[[Category:Bibtex| ]]
== BibTex ==
<bibtex>
@book{morv05,
editor = {Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Roel de Vrijer},
title = {Processes, Terms and Cycles: Steps on the Road to Infinity; Essays Dedicated to Jan Willem Klop on the Occasion on His 60th Birthday},
number = {LNCS3838},
series = {Festschrift},
publisher = {Springer--Verlag},
address = {Berlin Heidelberg},
year = {2005}
}
</bibtex>