News Background Topics Dates Submission Invited Speakers Program Program Committee Menu



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 17th International Workshop on Termination continues the successful workshops held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), Leipzig (2009), Edinburgh (2010), Obergurgl (2012), Bertinoro (2013), Vienna (2014), Obergurgl (2016), and Oxford (2018).

Workshop Topics

The 17th 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):

Important dates


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 the submission page:

Please, use LaTeX and the LIPIcs style file to prepare your submission.

Invited Speakers

Amir M. Ben-Amram.
Title: Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs

In Bound Analysis we are given a program and we seek functions that bound the growth of computed values, the running time, etc., in terms of input parameters. Problems of this type are uncomputable for ordinary, full languages, but may be solvable for weak languages, possibly representing an abstraction of a "real" program. In 2008, Jones, Kristiansen and I showed that, for a weak but non-trivial imperative programming language, it is possible to decide whether values are polynomially bounded. In this talk, I will focus on current work with Geoff Hamilton, where we show how to compute tight polynomial bounds (up to constant factors) for the same language. We have been able to do that as efficiently as possible, in the sense that our solution has polynomial space complexity, and we showed the problem to be PSPACE-hard. The analysis is a kind of abstract interpreter which computes in a domain of symbolic bounds plus just enough information about data-flow to correctly analyse loops. A salient point is how we solved the problem for multivariate bounds through the intermediary of univariate bounds. Another one is that the algorithm looks for worst-case lower bounds, but a completeness result shows that the maximum of these lower-bound functions is also an upper bound (up to a constant factor).


Click here to open the WST 2021 program. All times are in EDT (GMT-4).

Program Committee

Valid XHTML 1.0! Valid CSS!