WST Home Page

14th International Workshop on Termination (WST)

Overview

The Workshop on Termination 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-fertilisation 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 14th International Workshop on Termination in Vienna 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), and Bertinoro (2013). More information on earlier WSTs is available on the Termination Portal:

http://www.termination-portal.org/wiki/WST

Topics

The 14th International Workshop on Termination welcomes contributions on all aspects of termination and complexity analysis (and their automation) for various models of computation, ranging from rewrite systems and state transition systems to programming languages.

Contributions from the imperative, constraint, functional, logic, and concurrent programming communities, and papers investigating applications of complexity or termination (for example in program transformation or theorem proving) are particularly welcome.

Areas of interest include, but are not limited to, the following:

Termination of programs
Termination of rewriting
Termination analysis of transition systems
Complexity of programs
Complexity of rewriting
Implicit computational complexity
Implementation of termination and complexity analysis methods
SAT and SMT solving for (non-)termination analysis
Certification of termination and complexity proofs
Termination orders, well-founded orders, and reduction orders
Termination methods for theorem provers
Strong and weak normalisation of lambda calculi
Termination analysis for different language paradigms
Invariants for termination proving
Challenging termination problems
Applications to program transformation and compilation
Comparison and classification of termination methods
Non-termination and loop detection
Termination in distributed and concurrent systems
Proof methods for liveness and fairness
Well-quasi-order theory
Ordinal notations and subrecursive hierarchies

Organisation

Program Committee

Invited Talk

The keynote will be given by Jasmin Fisher, Microsoft Research and Department of Biochemistry, University of Cambridge, United Kingdom:

http://research.microsoft.com/~jfisher/

Title

Termination of Biological Programs

Abstract

Living cells are highly complex reactive systems operating under varying environmental conditions. By executing diverse cellular programs, cells are driven to acquire distinct cell fates and behaviours. Deciphering these programs is key to understanding how cells orchestrate their functions to create robust systems in health and disease. Due to the staggering complexity, this remains a major challenge. Stability in biological systems is a measure of the homeostatic nature and robustness against environmental perturbations. In computer science, stability means that the system will eventually reach a fixed point regardless of its initial state. Or, in other words, that all computations terminate with variables acquiring the same value regardless of the path that led to termination. Based on robust techniques to prove stabilization/termination in very large systems, we have developed an innovative platform called BMA that allows biologists to model and analyse biological signalling networks. BMA analyses systems for stabilization, searches for paths leading to stabilization, and allows for bounded model-checking and simulation, all with intelligible visualization of results. In this talk, I will summarize our efforts in this direction and talk about the application of termination analysis in drug discovery and cancer.

Joint work with Byron Cook, Nir Piterman, Samin Ishtiaq, Alex Taylor and Ben Hall.

Informal Proceedings

The informal proceedings of WST 2014 are available here: pdf

Accepted Papers

Harald Zankl, Sarah Winkler and Aart Middeldorp. Automating Elementary Interpretations
Étienne Payet and Fred Mesnard. Non-termination of Dalvik bytecode via compilation to CLP
Norbert Preining, Kazuhiro Ogata and Kokichi Futatsugi. Specifying and verifying liveness properties of QLOCK in CafeOBJ
Jan Leike and Matthias Heizmann. Geometric Series as Nontermination Arguments for Linear Lasso Programs
Byron Cook, Stephen Magill, Matthew Parkinson and Thomas Stroeder. Reducing Deadlock and Livelock Freedom to Termination
Raphael Rodrigues, Péricles Alves, Fernando Pereira and Laure Gonnord. Real-world loops are easy to predict : a case study
Nachum Dershowitz. Another Proof for the Recursive Path Ordering
Jeroen Ketema and Alastair Donaldson. Automatic Termination Analysis for GPU Kernels
Alfons Geser. A Solution to Endrullis-08 and Similar Problems
Joerg Endrullis and Hans Zantema. Non-termination using Regular Languages
Lars Hellström. Ordering Networks
Caterina Urban and Antoine Miné. To Infinity... and Beyond!
Naoki Nishida and Takumi Kataoka. On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants
Heidy Khlaaf, Byron Cook and Nir Piterman. Fairness for Infinite-State Systems
Martin Avanzini and Bertram Felgenhauer. Type Introduction for Runtime Complexity Analysis
Haruhiko Sato and Sarah Winkler. A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
Alexander Bau and Johannes Waldmann. Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling
Alfons Geser. Kurth's Criterion H Revisited
Dieter Hofbauer. On the derivational complexity of Kachinuki orderings

Call for Papers

Contact

Carsten Fuhs