VSL 2014: VIENNA SUMMER OF LOGIC 2014
WST Call for Papers

WST 2014 – 14th International Workshop on Termination
July 17-18, 2014 · Vienna, Austria

http://vsl2014.at/wst

Also available in plain text.

Objectives

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 constraint 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 normalization 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

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

Submission

Submissions are short papers / extended abstracts which should not exceed 5 pages using the LIPIcs style for LaTeX:

http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/

There will be no formal reviewing, but we will provide informal feedback for each submission. Accepted papers will be made available electronically, both on the WST 2014 web page and on the FLoC USB proceedings. The workshop proceedings are informal as well. Thus, submission to WST 2014 is not in conflict with an earlier, concurrent, or later publication of the same material at a journal, a conference, or another workshop. In case of simultaneous submissions to several FLoC events, please state in the abstract on easychair to which other FLoC venues you are submitting as well.

Papers should be submitted electronically via the submission page:

https://www.easychair.org/conferences/?conf=wst2014

Important Dates

Paper submission 30 April 2014
Notification 07 May 2014
Final versions due 21 May 2014
Workshop date 17 - 18 July 2014