[SMT-LIB] 2nd CfP: Workshop on Termination 2013

[Carsten Fuhs]

========= 13th International Workshop on Termination (WST) ===========

               http://www.imn.htwk-leipzig.de/WST2013/

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 13th  Workshop on Termination will  be held from August  29 to 31,
2013, at the Centro Residenziale Universitario di Bertinoro (Italy).

It  will be  a joint  workshop,  together with  the 3rd  International
Workshop on  Foundational and Practical Aspects  of Resource Analysis.
The  sessions  of  WST  and  FOPARA  will  be  interleaved,  this  way
facilitating the interaction between the two communities.


Invited Speaker: Byron Cook on  Beyond Termination

Abstract: So  we can  prove program termination.   Now what?   In this
talk I will discuss the development of tools that build on termination
proving techniques.

Bio:  Prof.  Dr.  Byron  Cook  is Principal  Researcher  at  Microsoft
Research, and Professor at University College London. Byron has worked
in  the   past  on  Haskell,  hardware   modelling  and  verification,
biological  systems  modelling  and  verification,  SAT/SMT,  symbolic
software model checking, temporal logics, and termination proving.


========= Important Dates ============================================

    submission:     July 15, 2013
    notification:   July 25, 2013
    final version:  August 10, 2013
    workshop:       August 29 - 31, 2013


========= Topics =====================================================

The 13th International  Workshop on Termination welcomes contributions
on all aspects of termination and complexity analysis.

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 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 systems
    Proof methods for liveness and fairness
    Well-quasi-order theory
    Ordinal notations and subrecursive hierarchies

========= Program Committee ==========================================

    Evelyne Contejean (Univ. Paris-Sud)
    Carsten Fuhs (Univ. College London)
    Alfons Geser (HTWK Leipzig)
    Jürgen Giesl (RWTH Aachen)
    Sergio Greco (Univ. of Calabria)
    Nao Hirokawa (JAIST)
    Dieter Hofbauer (ASW BA Saarland)
    Georg Moser (Univ. Innsbruck)
    Albert Rubio (Univ. Politecnica de Catalunya)
    Peter Schneider-Kamp (Syddansk Univ.)
    Johannes Waldmann (HTWK Leipzig) (chair)
    Florian Zuleger (TU Wien)

========= Submission =================================================

Submissions are short papers/extended abstract which should not exceed
5 pages.  There will be no  formal reviewing. Accepted  papers will be
made available electronically at the workshop.

Papers  should be  submitted  electronically via  the submission  page
http://www.easychair.org/conferences/?conf=wst2013

Final  versions should  be created  using LaTeX  and the  LIPIcs style
file.

========= Registration, Travel =======================================

All local arrangements are joint with   http://fopara2013.cs.unibo.it/