WST 2016
15th International Workshop on Termination
September 5-7, 2016, Obergurgl, Austria
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 term rewriting and from the different programming language communities. The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.
The 15th International Workshop on Termination in Obergurgl 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), and Vienna (2014). WST 2016 is part of the week-long event Computational Logic in the Alps. Information on earlier termination workshops is available on the Termination Portal.
Important Dates
| submission: | June 22, 2016 |
| notification: | July 12, 2016 |
| final version: | August 3, 2016 |
| workshop: | September 5 – 7, 2016 |
Topics
Topics of interest include all aspects of termination. This includes (but is not limited to):
- 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
- implicit computational complexity
- infinitary normalization
- non-termination analysis and loop detection
- normalization in lambda calculi
- operational termination of conditional rewrite 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
- well-founded relations and well-quasi-orders
Competition
There will be a live complexity and termination competition during the workshop, including time to present both the results and the tools of the participants.
Submission
We solicit short papers and extended abstracts of at most 5 pages in LIPIcs style. 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 must be submitted electronically via the EasyChair submission site.
Program Committee
| Ugo Dal Lago | Bologna University | |
| Jörg Endrullis | VU University Amsterdam | |
| Yukiyoshi Kameyama | University of Tsukuba | |
| Salvador Lucas | Universidad Politécnica de Valencia | |
| Aart Middeldorp | University of Innsbruck | (co-chair) |
| Thomas Ströder | RWTH Aachen | |
| René Thiemann | University of Innsbruck | (co-chair) |
| Andreas Weiermann | Ghent University |
Invited Speaker
| Reiner Hähnle | TU Darmstadt | (slides) Refined Resource Analysis Based on Cost Relations |
Program
There will be 13 regular presentations at WST 2016:
- Christophe Alias, Carsten Fuhs and Laure Gonnord
(slides) Estimation of Parallel Complexity with Rewriting Techniques - Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio
(slides) Proving termination through conditional termination - Marc Brockschmidt, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
(slides) Certifying Safety and Termination Proofs for Integer Transition Systems - Florian Frohn, Marc Brockschmidt and Jürgen Giesl
(slides) Automated Inference of Upper Complexity Bounds for Java Programs - Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt and Jürgen Giesl
(slides) Lower Runtime Bounds for Integer Programs - Carsten Fuhs
(slides) SMT-Based Techniques in Automated Termination Analysis - Alfons Geser, Johannes Waldmann and Mario Wenzel
(slides) Symbolic Enumeration of One-Rule String Rewriting Systems - Jera Hensel, Jürgen Giesl, Florian Frohn and Thomas Ströder
(slides) Termination Analysis of Programs with Bitvector Arithmetic by Symbolic Execution - Cynthia Kop
(slides) Non-deterministic Characterisations - Christian Sternagel
(slides) The Generalized Subterm Criterion in TTT2 - Thomas Sternagel and Christian Sternagel
(slides) A Characterization of Quasi-Decreasingness - Hans Zantema, Dennis Nolte and Barbara König
(slides) Termination of Term Graph Rewriting - Hans Zantema and Alexander Fedotov
(slides) Nontermination of string and cycle rewriting by automata
Proceedings