News
- WST 2021 will be Virtual
- The submission deadline was extended to May 9, 2021
- Registration is open now. The early registration deadline is the 4th of July. For detailed information about registration and fees, please see the CADE-28 website. Registration is conducted via ConfTool.
- The proceedings is available now: [PDF].
- Program. All times are in EDT (GMT-4).
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 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):
- 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
Important dates
- Submission deadline: April 25, 2021 May 9, 2021
- Notification: May 30, 2021 June 6, 2021
- Final version due: June 13, 2021 June 20, 2021
- Workshop: July 16, 2021
Submission
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:
https://easychair.org/conferences/?conf=wst2021
Please, use LaTeX and the LIPIcs style file to prepare your submission.
Invited Speakers
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).
Program Committee
- Martin Avanzini - INRIA Sophia, Antipolis
- Carsten Fuhs - Birkbeck, U. of London
- Samir Genaim (chair) - U. Complutense de Madrid
- Jürgen Giesl - RWTH Aachen
- Matthias Heizmann - U. of Freiburg
- Cynthia Kop - Radboud U. Nijmegen
- Salvador Lucas - U. Politècnica de València
- Étienne Payet - U. de La Réunion
- Albert Rubio - U. Complutense de Madrid
- René Thiemann - U. of Innsbruck