Termination-Portal.org - User contributions [en]

Termination Competition 2024

2024-01-26T09:25:01Z

Akihisa Yamada: /* Competition Categories */ dropped "discussed ..."

The Termination and Complexity Competition (termCOMP) 2024 will be affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024].

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before IJCAR, 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 IJCAR.


== Dates ==

TBA


== 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 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory, and the problem file name is given as the command line argument.
Extra info can be obtained from environment variables, cf. [[Termination Competition 2014 technical details]]

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

For those 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
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada, AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2023 ==

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

Proposed changes:

* we plan to introduce new categories for [https://github.com/orgs/TermCOMP/discussions/82 termination of probabilistic TRSs]
* we plan to use the new [https://github.com/orgs/TermCOMP/discussions/83 ARI format]

Adopted changes:

* To keep the tension high, the first run will not be public. Tool authors will be notified about technical problems and conflicting results.

Termination Competition

2023-09-12T08:36:29Z

Akihisa Yamada: /* Organization */ new organization

= 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 2023]] will be held in [[19th International Workshop on Termination]] in August 24, Obergurgl, Austria.

== 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://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid
* [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 [[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 [[Transition_Systems|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[C_Integer_Programs|termination of C integer programs]]
* [[Cycle_Rewriting|termination of cycle rewriting]]

== 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 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".

== Static Backups of Results ==

For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].

Termination Competition 2023

2023-09-12T08:32:05Z

Akihisa Yamada: /* Status */

The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with [[WST2023|WST 2023]].

The competition will be run on the [http://www.starexec.org/ StarExec platform].
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.

All (co-)authors of tools or benchmarks are encouraged (but not required) to give a 5-20min presentation of their contributions at WST 2023.
To do so, we ask for a title and abstract by 15 June via [https://easychair.org/conferences/?conf=wst23 this submission site].
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).

== Status ==
[https://termcomp.github.io/Y2023/ Status]

== Dates ==

* June 15: (Optional) Title and Abstract Submission [https://easychair.org/conferences/?conf=wst23 to WST]
* July 1: (Optional) Paper Submission
* Aug. 6: Tool and Benchmark Submission
* Aug. 13: First Run
* Aug. 20: Bugfix Deadline
* Aug. 24 (CET): Final Run
* Aug. 24-25 (CET): WST

== Competition Categories ==

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory, and the problem file name is given as the command line argument.
Extra info can be obtained from environment variables, cf. [[Termination Competition 2014 technical details]]

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

For those 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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2022 ==

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

Proposed changes:

Adopted changes:

19th International Workshop on Termination

2023-08-15T13:32:26Z

Akihisa Yamada: /* Program */

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

As part of [http://cl-informatik.uibk.ac.at/events/osr-2023/ Obergurgl Summer on Rewriting 2023] and
co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
{|
|-
|style="vertical-align:top;"|14:00
| [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski]:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)
{|
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===

'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)
{|
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

'''Session 4''': Non-Termination (Chair: René Thiemann)
{|
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
{|
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
{|
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| [https://akihisayamada.github.io/ Akihisa Yamada]:
'''Results of the [[Termination Competition 2023]]'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-15T13:29:08Z

Akihisa Yamada: links

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

As part of [http://cl-informatik.uibk.ac.at/events/osr-2023/ Obergurgl Summer on Rewriting 2023] and
co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
{|
|-
|style="vertical-align:top;"|14:00
| [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski]:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)
{|
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===

'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)
{|
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

'''Session 4''': Non-Termination (Chair: René Thiemann)
{|
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
{|
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
{|
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet]:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| [https://akihisayamada.github.io/ Akihisa Yamada]:
'''Results of the [[Termination Competition 2023]]'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

Termination Competition 2023

2023-08-14T12:18:43Z

Akihisa Yamada: /* Competition Procedure */

The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with [[WST2023|WST 2023]].

The competition will be run on the [http://www.starexec.org/ StarExec platform].
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.

All (co-)authors of tools or benchmarks are encouraged (but not required) to give a 5-20min presentation of their contributions at WST 2023.
To do so, we ask for a title and abstract by 15 June via [https://easychair.org/conferences/?conf=wst23 this submission site].
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).

== Status ==
[https://termcomp.herokuapp.com/Y2023/ Status]

== Dates ==

* June 15: (Optional) Title and Abstract Submission [https://easychair.org/conferences/?conf=wst23 to WST]
* July 1: (Optional) Paper Submission
* Aug. 6: Tool and Benchmark Submission
* Aug. 13: First Run
* Aug. 20: Bugfix Deadline
* Aug. 24 (CET): Final Run
* Aug. 24-25 (CET): WST

== Competition Categories ==

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory, and the problem file name is given as the command line argument.
Extra info can be obtained from environment variables, cf. [[Termination Competition 2014 technical details]]

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

For those 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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2022 ==

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

Proposed changes:

Adopted changes:

19th International Workshop on Termination

2023-08-14T11:12:03Z

Akihisa Yamada: map link

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

As part of [http://cl-informatik.uibk.ac.at/events/osr-2023/ Obergurgl Summer on Rewriting 2023] and
co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
{|
|-
|style="vertical-align:top;"|14:00
| Benjamin Kaminski:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)
{|
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===

'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)
{|
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

'''Session 4''': Non-Termination (Chair: René Thiemann)
{|
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| Etienne Payet:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
{|
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
{|
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and Etienne Payet:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| Akihisa Yamada:
'''Results of the Termination Competition 2023'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-14T11:05:47Z

Akihisa Yamada: registration is not open

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.

As part of [http://cl-informatik.uibk.ac.at/events/osr-2023/ Obergurgl Summer on Rewriting 2023] and
co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
{|
|-
|style="vertical-align:top;"|14:00
| Benjamin Kaminski:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)
{|
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===

'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)
{|
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

'''Session 4''': Non-Termination (Chair: René Thiemann)
{|
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| Etienne Payet:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
{|
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
{|
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and Etienne Payet:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| Akihisa Yamada:
'''Results of the Termination Competition 2023'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-14T09:30:38Z

Akihisa Yamada: /* Program */

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

Registration is open at [http://cl-informatik.uibk.ac.at/events/osr-2023/ OSR 2023 website]!

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

'''Session 1''': Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
{|
|-
|style="vertical-align:top;"|14:00
| Benjamin Kaminski:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 2''': Termination of Term Rewriting (Chair: Johannes Waldmann)
{|
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===

'''Session 3''': Termination beyond Term Rewriting (Chair: Carsten Fuhs)
{|
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

'''Session 4''': Non-Termination (Chair: René Thiemann)
{|
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| Etienne Payet:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

'''Session 5''': Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
{|
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

'''Session 6''': termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
{|
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and Etienne Payet:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| Akihisa Yamada:
'''Results of the Termination Competition 2023'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-14T09:22:26Z

Akihisa Yamada: Program

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

Registration is open at [http://cl-informatik.uibk.ac.at/events/osr-2023/ OSR 2023 website]!

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract
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.

==Program==

===Thursday 24 August===

{|
|colspan="2"|Session 1: Keynote & Probabilistic Termination (Chair: Akihisa Yamada)
|-
|style="vertical-align:top;"|14:00
| Benjamin Kaminski:
'''Termination of Probabilistic Programs (invited talk)'''
|-
|style="vertical-align:top;"|15:00
| Jan-Christoph Kassing and Jürgen Giesl:
'''Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting''' [https://doi.org/10.48550/arXiv.2307.10002 (paper)]
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

{|
|colspan="2"|Session 2: Termination of Term Rewriting (Chair: Johannes Waldmann)
|-
|style="vertical-align:top;"|16:00
| Fabian Mitterwallner, Aart Middeldorp and René Thiemann:
'''Linear Termination over N is Undecidable''' [https://doi.org/10.48550/arXiv.2307.14805 (paper)]
|-
|style="vertical-align:top;"|16:30
| Teppei Saito and Nao Hirokawa:
'''Generalizing Weighted Path Orders''' [https://doi.org/10.48550/arXiv.2307.13973 (paper)]
|-
|style="vertical-align:top;"|17:00
| René Thiemann and Elias Wenninger:
'''A Verified Efficient Implementation of the Weighted Path Order''' [https://doi.org/10.48550/arXiv.2307.14671 (paper)]
|-
|style="vertical-align:top;"|17:30
| Nao Hirokawa and Aart Middeldorp:
'''Hydra Battles and AC Termination, Revisited''' [https://doi.org/10.48550/arXiv.2307.14036 (paper)]
|-
|18:00
|
----
|}

===Friday 25 August===
{|
|colspan="2"|Session 3: Termination beyond Term Rewriting (Chair: Carsten Fuhs)
|-
|style="vertical-align:top;"|9:00
| Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin:
'''On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic''' [https://doi.org/10.48550/arXiv.2307.14094 (paper)]
|-
|style="vertical-align:top;"|9:30
| Liye Guo and Cynthia Kop:
'''Higher-Order LCTRSs and Their Termination''' [https://doi.org/10.48550/arXiv.2307.13519 (paper)]
|-
|style="vertical-align:top;"|10:00
| Jera Hensel and Jürgen Giesl:
'''Automated Termination Proofs for C Programs with Lists''' [https://doi.org/10.48550/arXiv.2307.11024 (paper)]
|-
|style="vertical-align:top;"|10:30
| coffee break
|}

{|
|colspan="2"|Session 4: Non-Termination (Chair: René Thiemann)
|-
|style="vertical-align:top;"|11:00
| Dieter Hofbauer and Johannes Waldmann:
'''Old and New Benchmarks for Relative Termination of String Rewrite Systems''' [https://doi.org/10.48550/arXiv.2307.14149 (paper)]
|-
|style="vertical-align:top;"|11:30
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination by Acceleration Driven Clause Learning''' [https://doi.org/10.48550/arXiv.2307.09839 (paper)]
|-
|style="vertical-align:top;"|12:00
| Etienne Payet:
'''Binary Non-Termination in Term Rewriting and Logic Programming''' [https://doi.org/10.48550/arXiv.2307.11549 (paper)]
|-
|style="vertical-align:top;"|12:30
| lunch
|}

{|
|colspan="2"|Session 5: Complexity Analysis and Probabilistic termCOMP (Chair: Benjamin Kaminski)
|-
|style="vertical-align:top;"|14:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops''' [https://doi.org/10.48550/arXiv.2307.10061 (paper)]
|-
|style="vertical-align:top;"|14:30
| Cynthia Kop and Deivid Vale:
'''Complexity Analysis for Call-by-Value Higher-Order Rewriting''' [https://doi.org/10.48550/arXiv.2307.13426 (paper)]
|-
|style="vertical-align:top;"|15:00
| '''0th Probabilistic termCOMP'''
|-
|style="vertical-align:top;"|15:30
| coffee break
|}

{|
|colspan="2"|Session 6: termCOMP 2023 and business meeting (Chair: Akihisa Yamada)
|-
|style="vertical-align:top;"|16:00
| Nils Lommen, Eleanore Meyer and Jürgen Giesl:
'''KoAT: An Automatic Complexity Analysis Tool for Integer Programs'''
|-
|style="vertical-align:top;"|16:15
| Florian Frohn and Jürgen Giesl:
'''Proving Non-Termination and Lower Runtime Bounds via ADCL with LoAT'''
|-
|style="vertical-align:top;"|16:30
| Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Florian Frohn, Carsten Fuhs, Jera Hensel, Jan-Christoph Kassing, Nils Lommen and Eleanore Meyer:
'''AProVE 2023'''
|-
|style="vertical-align:top;"|16:45
| Fred Mesnard and Etienne Payet:
'''NTI+cTI: a Logic Programming Termination Analyzer'''
|-
|style="vertical-align:top;"|17:00
| Dieter Hofbauer:
'''MultumNonMulta entering Term Rewriting'''
|-
|style="vertical-align:top;"|17:15
| Akihisa Yamada:
'''Results of the Termination Competition 2023'''
|-
|style="vertical-align:top;"|17:30
| '''business meeting'''
|}

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-14T07:51:30Z

Akihisa Yamada: /* Keynote Speaker */

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

Registration is open at [http://cl-informatik.uibk.ac.at/events/osr-2023/ OSR 2023 website]!

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

[https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.
Termination of Probabilistic Programs

Abstract 
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.

==Accepted Papers==

* Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin. On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
* Teppei Saito and Nao Hirokawa. Generalizing Weighted Path Orders
* Nils Lommen, Eleanore Meyer and Jürgen Giesl. Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
* Florian Frohn and Jürgen Giesl. Proving Non-Termination by Acceleration Driven Clause Learning
* Etienne Payet. Binary Non-Termination in Term Rewriting and Logic Programming
* René Thiemann and Elias Wenninger. A Verified Efficient Implementation of the Weighted Path Order
* Jan-Christoph Kassing and Jürgen Giesl. Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
* Jera Hensel and Jürgen Giesl. Automated Termination Proofs for C Programs with Lists
* Liye Guo and Cynthia Kop. Higher-Order LCTRSs and Their Termination
* Nao Hirokawa and Aart Middeldorp. Hydra Battles and AC Termination, Revisited
* Dieter Hofbauer and Johannes Waldmann. Old and New Benchmarks for Relative Termination of String Rewrite Systems
* Fabian Mitterwallner, Aart Middeldorp and René Thiemann. Linear Termination over N is Undecidable
* Cynthia Kop and Deivid Vale. Complexity Analysis for Call-by-Value Higher-Order Rewriting

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: <s>July 27</s>
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-08-14T07:46:32Z

Akihisa Yamada: /* Important Dates */

Termination Competition 2023

2023-07-19T09:01:06Z

Akihisa Yamada: link to status

The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with [[WST2023|WST 2023]].

The competition will be run on the [http://www.starexec.org/ StarExec platform].
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.

All (co-)authors of tools or benchmarks are encouraged (but not required) to give a 5-20min presentation of their contributions at WST 2023.
To do so, we ask for a title and abstract by 15 June via [https://easychair.org/conferences/?conf=wst23 this submission site].
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).

== Status ==
[https://termcomp.herokuapp.com/Y2023/ Status]

== Dates ==

* June 15: (Optional) Title and Abstract Submission [https://easychair.org/conferences/?conf=wst23 to WST]
* July 1: (Optional) Paper Submission
* Aug. 6: Tool and Benchmark Submission
* Aug. 13: First Run
* Aug. 20: Bugfix Deadline
* Aug. 24 (CET): Final Run
* Aug. 24-25 (CET): WST

== Competition Categories ==

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2022 ==

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

Proposed changes:

Adopted changes:

Termination Competition

2023-07-18T07:47:16Z

Akihisa Yamada: /* Upcoming Competitions */

= 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 2023]] will be held in [[19th International Workshop on Termination]] in August 24, Obergurgl, Austria.

== 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], 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
* [https://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid
* [https://group-mmm.org/~ayamada/ Akihisa Yamada] (Chair), 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 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.

== 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 [[Transition_Systems|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[C_Integer_Programs|termination of C integer programs]]
* [[Cycle_Rewriting|termination of cycle rewriting]]

== 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 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".

== Static Backups of Results ==

For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].

19th International Workshop on Termination

2023-06-20T12:48:31Z

Akihisa Yamada: registration

Termination Portal

2023-06-16T04:51:00Z

Akihisa Yamada: /* Recent News */

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=
* [[Termination Competition 2023]]
* [[19th International Workshop on Termination]]
* [[Termination Competition 2022]]
<DynamicPageList>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</DynamicPageList>
Older news entries can be found on the [[:Category:News|news page]].

19th International Workshop on Termination

2023-06-16T02:47:26Z

Akihisa Yamada: Accepted papers

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

* [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.

==Accepted Papers==

* Ayuka Matsumi, Naoki Nishida, Misaki Kojima and Donghoon Shin. On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
* Teppei Saito and Nao Hirokawa. Generalizing Weighted Path Orders
* Nils Lommen, Eleanore Meyer and Jürgen Giesl. Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
* Florian Frohn and Jürgen Giesl. Proving Non-Termination by Acceleration Driven Clause Learning
* Etienne Payet. Binary Non-Termination in Term Rewriting and Logic Programming
* René Thiemann and Elias Wenninger. A Verified Efficient Implementation of the Weighted Path Order
* Jan-Christoph Kassing and Jürgen Giesl. Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
* Jera Hensel and Jürgen Giesl. Automated Termination Proofs for C Programs with Lists
* Liye Guo and Cynthia Kop. Higher-Order LCTRSs and Their Termination
* Nao Hirokawa and Aart Middeldorp. Hydra Battles and AC Termination, Revisited
* Dieter Hofbauer and Johannes Waldmann. Old and New Benchmarks for Relative Termination of String Rewrite Systems
* Fabian Mitterwallner, Aart Middeldorp and René Thiemann. Linear Termination over N is Undecidable
* Cynthia Kop and Deivid Vale. Complexity Analysis for Call-by-Value Higher-Order Rewriting

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: <s>June 15</s>
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-06-10T16:19:09Z

Akihisa Yamada: /* Important Dates */

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

* [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: <s>June 1</s>
* paper submission: <s>June 8</s>
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-05-30T09:44:41Z

Akihisa Yamada: /* Important Dates */

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

* [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* title and abstract submission: '''June 1'''
* paper submission: '''June 8'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-05-17T02:55:32Z

Akihisa Yamada: link to Obergurgl

August 24-25, 2023, [https://www.uibk.ac.at/uz-obergurgl/index.html.en University Center Obergurgl], Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

* [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-05-17T02:52:51Z

Akihisa Yamada: keynote speaker

August 24-25, 2023, Obergurgl, Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Keynote Speaker==

* [https://quave.cs.uni-saarland.de/benjamin-kaminski/ Benjamin Kaminski], Saarland U.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

Termination Competition 2023

2023-05-15T10:28:49Z

Akihisa Yamada: Created page with "The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with WST 2023. The competition will be run on the [http://www.starexec.org/ StarExec..."

The Termination and Complexity Competition (termCOMP) 2023 will be affiliated with [[WST2023|WST 2023]].

The competition will be run on the [http://www.starexec.org/ StarExec platform].
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.

All (co-)authors of tools or benchmarks are encouraged (but not required) to give a 5-20min presentation of their contributions at WST 2023.
To do so, we ask for a title and abstract by 1 June via [https://easychair.org/conferences/?conf=wst23 this submission site].
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).

== Dates ==

* June 1: (Optional) Title and Abstract Submission [https://easychair.org/conferences/?conf=wst23 to WST]
* July 1: (Optional) Paper Submission
* Aug. 6: Tool and Benchmark Submission
* Aug. 13: First Run
* Aug. 20: Bugfix Deadline
* Aug. 24 (CET): Final Run
* Aug. 24-25 (CET): WST

== Competition Categories ==

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2022 ==

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

Proposed changes:

Adopted changes:

19th International Workshop on Termination

2023-04-19T08:15:14Z

Akihisa Yamada:

August 24-25, 2023, Obergurgl, Austria.
Co-located with [http://cl-informatik.uibk.ac.at/iwc/2023/ IWC 2023].

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-04-19T06:18:08Z

Akihisa Yamada: Submission guidelines

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Submission Guidelines==

Submissions are short papers/extended abstracts which should not exceed 5 pages.
There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers
submitted elsewhere. The program committee checks relevance and provides additional feedback for each submission.
The accepted papers will be made available electronically before the workshop.

Papers should be submitted electronically via
[https://easychair.org/my/conference?conf=wst2023 the submission page].

Please use LaTeX and
[https://www.dagstuhl.de/en/publishing/series/details/LIPIcs the LIPIcs style file]
to prepare your submission.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-04-19T06:09:07Z

Akihisa Yamada: /* Important Dates */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-04-19T06:03:54Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* review feedback: July 6
* final version: July 27
* workshop: August 24-25

==Program Committee==

* [http://www-sop.inria.fr/members/Martin.Avanzini/ Martin Avanzini], INRIA Sophia Antipolis
* [https://ffrohn.github.io/ Florian Frohn], RWTH Aachen
* [https://www.dcs.bbk.ac.uk/~carsten/ Carsten Fuhs], Birkbeck, U. London
* [https://raulgut.github.io/ Raúl Gutiérrez], U. Politécnica de Madrid
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], U. La Réunion
* [https://costa.fdi.ucm.es/~arubio/ Albert Rubio], Complutense U. Madrid
* [http://cl-informatik.uibk.ac.at/users/thiemann/ René Thiemann], U. Innsbruck
* [https://deividrvale.github.io/ Deivid Vale], Radboud U. Nijmegen
* [https://www.imn.htwk-leipzig.de/~waldmann/index.html Johannes Waldmann], HTWK Leipzig
* [https://akihisayamada.github.io/ Akihisa Yamada], AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-04-19T05:55:47Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* review feedback: July 6
* final version: July 27
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Albert Rubio, Complutense U. Madrid
* René Thiemann, U. Innsbruck
* Deivid Vale, Radboud U. Nijmegen
* Johannes Waldmann, HTWK Leipzig
* Akihisa Yamada, AIST Tokyo Waterfront (chair)

19th International Workshop on Termination

2023-04-19T05:54:35Z

Akihisa Yamada: /* Important Dates */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract and paper): '''June 1'''
* notification: '''June 15'''
* review feedback: July 6
* final version: July 27
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Albert Rubio, Complutense U. Madrid
* René Thiemann, U. Innsbruck
* Johannes Waldmann, HTWK Leipzig
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-14T09:02:02Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Albert Rubio, Complutense U. Madrid
* René Thiemann, U. Innsbruck
* Johannes Waldmann, HTWK Leipzig
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-12T15:42:06Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Albert Rubio, Complutense U. Madrid
* René Thiemann, U. Innsbruck
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-12T15:40:32Z

Akihisa Yamada:

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination (WST 2023) continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* René Thiemann, U. Innsbruck
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-12T08:06:03Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* René Thiemann, U. Innsbruck
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-11T07:42:07Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Florian Frohn, RWTH Aachen
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Akihisa Yamada, AIST Tokyo Waterfront (chair)
* ...

19th International Workshop on Termination

2023-04-11T07:29:22Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Martin Avanzini, INRIA Sophia Antipolis
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Akihisa Yamada, AIST (chair)
* ...

WST2023

2023-04-10T01:14:23Z

Akihisa Yamada: Redirected page to 19th International Workshop on Termination

#REDIRECT [[19th International Workshop on Termination]]

19th International Workshop on Termination

2023-04-10T01:03:41Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* Akihisa Yamada, AIST (chair)
* ...

19th International Workshop on Termination

2023-04-08T11:23:47Z

Akihisa Yamada: /* Program Committee */

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Akihisa Yamada, AIST (chair)
* Carsten Fuhs, Birkbeck, U. London
* Raúl Gutiérrez, U. Politécnica de Madrid
* Étienne Payet, U. La Réunion
* ...

Termination Portal

2023-01-25T08:45:44Z

Akihisa Yamada: /* Recent News */

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=
* [[19th International Workshop on Termination]]
* [[Termination Competition 2022]]
<DynamicPageList>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</DynamicPageList>
Older news entries can be found on the [[:Category:News|news page]].

People:Akihisa Yamada

2023-01-25T08:43:29Z

Akihisa Yamada: update affiliation

{{Person
|firstname=Akihisa
|middlenames=
|lastname=Yamada
|titles=
|email=ayamada@trs.cm.nagoya-u.ac.jp
|homepage=https://akihisayamada.github.io/
|country=Japan
|university=National Institute of Advanced Industrial Science and Technology (AIST)
|department=Cyber Physical Security Reserch Center
|role=senior researcher
}}

19th International Workshop on Termination

2023-01-25T08:25:18Z

Akihisa Yamada: location information

August 24-25, 2023, Obergurgl, Austria.
Co-located with IWC 2023.

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Akihisa Yamada, AIST (chair)
* TBA...

19th International Workshop on Termination

2023-01-16T02:07:17Z

Akihisa Yamada:

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): May 7
* submission (paper): May 14
* notification: June 11
* workshop: August 24-25

==Program Committee==

* Akihisa Yamada, AIST (chair)
* TBA...

19th International Workshop on Termination

2023-01-16T01:56:51Z

Akihisa Yamada:

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* termination and complexity analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, probabilistic programs, etc.)
* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): Sunday, 7th May
* submission (paper): Sunday, 14th May
* notification: Sunday, 11th June
* workshop: Friday, 25th August

==Program Committee==

* Akihisa Yamada, AIST (chair)
* TBA...

19th International Workshop on Termination

2023-01-16T01:37:45Z

Akihisa Yamada: Created page with "==Background== The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this int..."

==Background==

The Workshop on Termination (WST) traditionally 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-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The 19th International Workshop on Termination continues
the successful workshops held in
St. Andrews (1993),
La Bresse (1995),
Ede ([http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 1997]),
Dagstuhl ([http://verify.rwth-aachen.de/giesl/WST99.html 1999]),
Utrecht ([http://www.cs.tau.ac.il/~nachumd/wst/index.html 2001]),
Valencia ([http://users.dsic.upv.es/~rdp03/wst/ 2003]),
Aachen ([http://www-i2.informatik.rwth-aachen.de/WST04/ 2004]),
Seattle ([https://www.illc.uva.nl/LogicList/newsitem.php?id=1416 2006]),
Paris ([http://www.lsv.fr/Events/rdp07/wst.html 2007]),
Leipzig ([http://www.imn.htwk-leipzig.de/~waldmann/wst09/cfp/WST09_cfp.pdf 2009]),
Edinburgh ([http://www.floc-conference.org/WST-home.html 2010]),
Obergurgl ([http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ 2012]),
Bertinoro ([http://www.imn.htwk-leipzig.de/WST2013/ 2013]),
Vienna ([http://easychair.org/smart-program/VSL2014/WST-index.html 2014]),
Obergurgl ([http://cl-informatik.uibk.ac.at/events/wst-2016/ 2016]),
Oxford ([http://wst2018.webs.upv.es/ 2018]),
virtually ([http://costa.fdi.ucm.es/wst2021/ 2021]), and
Haifa ([https://sws.cs.ru.nl/WST2022 2022]).

==Workshop Topics==

The 19th International Workshop on Termination welcomes contributions
on all aspects of termination. In particular, papers investigating applications
of termination (for example in complexity analysis, program analysis and
transformation, theorem proving, program correctness, modeling computational
systems, etc.) are very welcome.

Topics of interest include (but are not limited to):

* abstraction methods in termination analysis
* certification of termination and complexity proofs
* challenging termination problems
* comparison and classification of termination methods
* complexity analysis in any domain
* implementation of termination and complexity methods
* non-termination analysis and loop detection
* normalization and infinitary normalization
* operational termination of logic-based systems
* ordinal notation and subrecursive hierarchies
* SAT, SMT, and constraint solving for (non-)termination analysis
* scalability and modularity of termination methods
* termination analysis in any domain (lambda calculus, declarative programming, rewriting, transition systems, etc.)
* well-founded relations and well-quasi-orders

==Termination Competition==

Since 2003, the catalytic effect of WST to stimulate new research
on termination has been enhanced by the celebration of the [[Termination_Competition]]
and its continuously developing problem databases containing thousands of programs
as challenges for termination analysis in different categories.
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.

==Important Dates==

* submission (abstract): Sunday, 7th May
* submission (paper): Sunday, 14th May
* notification: Sunday, 11th June
* workshop: Friday, 25th August

==Program Committee==

* Akihisa Yamada, AIST (chair)
* TBA...

WST

2023-01-16T01:36:04Z

Akihisa Yamada: added 2023 link

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:
* [[19th International Workshop on Termination]], Obergurgl, Austria, August 24-25, 2023.

Previous workshops:
* [https://sws.cs.ru.nl/WST2022 18th International Workshop on Termination] during [https://www.floc2022.org/ Federated Logic Conference (FLoC)], Haifa, Israel, August 11-12, 2022.
* [http://costa.fdi.ucm.es/wst2020/ 17th International Workshop on Termination] planned to be co-located with IJCAR and [http://fscdconference.org/editions/upcoming FSCD 2020], Paris (France), June/July, 2020.
* [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.
* [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.
* [https://easychair.org/smart-program/VSL2014/WST-index.html 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].
* [https://portal.imn.htwk-leipzig.de/termine/10-international-workshop-on-termination/ 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 Termination, Seattle, 2006].
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Termination, Aachen, 2004].
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Termination, Valencia, 2003].
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Termination, Utrecht, 2001].
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Termination, 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]]

Termination Competition 2022

2022-07-26T11:28:52Z

Akihisa Yamada: link to the first run

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

Five medals will be awarded:
* Gold, Silver, and Bronze medals go to the top three teams according to a competition-wide ranking.
* Two special medals go to the best two teams in advancing the state of the art.

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before FLoC, 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 FLoC.

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.
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).

== Status ==

[https://termcomp.github.io/Y2022/ first run]

== Dates ==

* <s>June 18</s>: (Optional) <s>Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]</s>
* July 24: Tools and Problems Submission Deadline
* July 25: First Run
* July 30: Conflict/Bug Report Deadline
* Aug. 4: Bugfix Deadline
* Aug. 7 <s>5</s>: Final Run
* Aug. 9: Award Ceremony at FLoC
* Aug. 12: Presentations at WST

== Awards and Competition Categories ==

Five [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.
* 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.

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

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2021 ==

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

Proposed changes:

Adopted changes:
* Medals will be awarded.
* A competition-wide ranking scheme based on Euclidean norm.
* Awards for the two best solvers in advancing the state of the art (closing unsolved termination problems or improving known complexity bounds).
* Tool/benchmark authors are invited to submit a paper and present at WST.

Termination Competition 2022

2022-07-19T06:26:26Z

Akihisa Yamada: Details of the ranking

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

Five medals will be awarded:
* Gold, Silver, and Bronze medals go to the top three teams according to a competition-wide ranking.
* Two special medals go to the best two teams in advancing the state of the art.

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before FLoC, 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 FLoC.

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.
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).

== Dates ==

* <s>June 18</s>: (Optional) <s>Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]</s>
* July 24: Tools and Problems Submission Deadline
* July 25: First Run
* July 30: Conflict/Bug Report Deadline
* Aug. 4: Bugfix Deadline
* Aug. 7 <s>5</s>: Final Run
* Aug. 9: Award Ceremony at FLoC
* Aug. 12: Presentations at WST

== Awards and Competition Categories ==

Five [https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.
* 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.

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

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2021 ==

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

Proposed changes:

Adopted changes:
* Medals will be awarded.
* A competition-wide ranking scheme based on Euclidean norm.
* Awards for the two best solvers in advancing the state of the art (closing unsolved termination problems or improving known complexity bounds).
* Tool/benchmark authors are invited to submit a paper and present at WST.

Termination Competition 2022

2022-07-18T09:30:15Z

Akihisa Yamada: Changed final run date to 7 Aug. to avoid FLoC excursion day

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].
Five medals will be awarded, following a ranking scheme which is to be announced.

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before FLoC, 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 FLoC.

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.
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).

== Dates ==

* <s>June 18</s>: (Optional) <s>Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]</s>
* July 24: Tools and Problems Submission Deadline
* July 25: First Run
* July 30: Conflict/Bug Report Deadline
* Aug. 4: Bugfix Deadline
* Aug. 7 <s>5</s>: Final Run
* Aug. 9: Award Ceremony at FLoC
* Aug. 12: Presentations at WST

== Awards and Competition Categories ==

[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.
The number of medals and the ranking scheme will be announced soon.

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2021 ==

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

Proposed changes:
* A competition-wide ranking scheme following SMT-COMP
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)
* The best new comer award
* The most improved tool award

Adopted changes:
* Medals will be awarded.
* Tool/benchmark authors are invited to submit a paper and present at WST.

Termination Competition 2022

2022-06-21T02:15:09Z

Akihisa Yamada: /* Dates */ added (optional) and <s> old date

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].
Five medals will be awarded, following a ranking scheme which is to be announced.

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before FLoC, 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 FLoC.

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.
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).

== Dates ==

* <s>June 18</s>: (Optional) <s>Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]</s>
* July 24: Tools and Problems Submission Deadline
* July 25: First Run
* July 30: Conflict/Bug Report Deadline
* Aug. 4: Bugfix Deadline
* Aug. 5: Final Run
* Aug. 9: Award Ceremony at FLoC
* Aug. 12: Presentations at WST

== Awards and Competition Categories ==

[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.
The number of medals and the ranking scheme will be announced soon.

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2021 ==

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

Proposed changes:
* A competition-wide ranking scheme following SMT-COMP
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)
* The best new comer award
* The most improved tool award

Adopted changes:
* Medals will be awarded.
* Tool/benchmark authors are invited to submit a paper and present at WST.

Termination Competition 2022

2022-06-21T02:12:38Z

Akihisa Yamada: number of medals = 5

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].
Five medals will be awarded, following a ranking scheme which is to be announced.

The competition will be run on the [http://www.starexec.org/ StarExec platform].
The first run will be shortly before FLoC, 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 FLoC.

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.
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).

== Dates ==

* June 18: Title and Abstract Submission [https://easychair.org/conferences/?conf=wst22 to WST]
* July 24: Tools and Problems Submission Deadline
* July 25: First Run
* July 30: Conflict/Bug Report Deadline
* Aug. 4: Bugfix Deadline
* Aug. 5: Final Run
* Aug. 9: Award Ceremony at FLoC
* Aug. 12: Presentations at WST

== Awards and Competition Categories ==

[https://www.floc2022.org/floc-olympic-games FLoC Olympic Games] medals will be awarded to participants.
The number of medals and the ranking scheme will be announced soon.

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

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].

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

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [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, RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Albert Rubio, Complutense University of Madrid
* Akihisa Yamada (Chair and Organizer), AIST Tokyo Waterfront

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/starexec-master/ the TermCOMP web repository].

To submit a benchmark, please follow the instruction at [https://github.com/TermCOMP/TPDB TPDB repository].

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.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

This refers to StarExec in general, and not to Termination or Complexity in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://github.com/StarExec/StarExec/issues issue tracker]
* [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])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Details ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/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 (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_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 2021 ==

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

Proposed changes:
* A competition-wide ranking scheme following SMT-COMP
* An award for the tool which advanced the state of the art the most (closing unsolved termination problems or improving known complexity bounds)
* The best new comer award
* The most improved tool award

Adopted changes:
* Medals will be awarded.
* Tool/benchmark authors are invited to submit a paper and present at WST.

Termination Competition

2022-06-17T06:00:25Z

Akihisa Yamada: Florian, you deleted you name :)

= 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 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].

== 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], 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
* [https://www.cs.upc.edu/~albert/ Albert Rubio], Complutense University of Madrid
* [https://group-mmm.org/~ayamada/ Akihisa Yamada] (Chair), 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 on, the organizer is Akihisa Yamada. Jobs are run on Star-Exec.

== 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 [[Transition_Systems|integer transition systems]] (since 2014)
* [[ITRS|integer term rewriting]] (since 2014)
* [[C_Integer_Programs|termination of C integer programs]]
* [[Cycle_Rewriting|termination of cycle rewriting]]

== 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 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".

== Static Backups of Results ==

For many previous competitions, static backups of the results are available [https://aprove-developers.github.io/termcomp_results/ here].