13th International Workshop on Termination (WST)
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 22, 2013
- notification: July 25, 2013
- early registration: August 8, 2013
- final version: August 10, 2013
- workshop: August 28 - 31, 2013
Program,
Proceedings
Accepted Papers
- Nachum Dershowitz:
Dependency Pairs are a Simple Semantic Path Ordering
(pdf)
- Akihisa Yamada, Keiichirou Kusakari and Toshiki Sakabe:
Partial Status for KBO
(pdf)
- Nachum Dershowitz:
The Ordinal Path Ordering
(pdf)
- Marco Calautti, Sergio Greco, Cristian Molinaro and Irina Trubitsyna:
Towards decidable classes of logic programs with function symbols
(pdf)
- Alexander Bau, Jörg Endrullis and Johannes Waldmann:
SAT compilation for Termination Proofs via Semantic Labelling
(pdf)
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs and Jürgen Giesl:
Analyzing Runtime and Size Complexity of Integer Programs
(pdf)
- Caterina Urban:
Piecewise-Defined Ranking Functions
(pdf)
- Marcus Ermler:
SAT-Based Loop Detection in Graph Rewriting
(pdf)
- Dieter Hofbauer:
Synthesizing matrix interpretations via backward completion
(pdf)
- Martin Avanzini, Michael Schaper and Georg Moser:
Small Polynomial Path Orders in TcT
(pdf)
- Cynthia Kop:
Termination of LCTRSs
(pdf)
- Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio:
Program Termination analysis using MAX-SMT
(pdf)
- Naohi Eguchi:
Predicative Lexicographic Path Orders: A Maximal Model for Primitive Recursive Functions
(pdf)
- Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn:
Automated nontermination proofs by safety proofs
(pdf)
- Stéphane Gimenez:
Towards Generic Inductive Constructions in Systems of Nets
(pdf)
- Marc Brockschmidt, Byron Cook and Carsten Fuhs:
Cooperation For Better Termination Proving
(pdf)
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
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.
Final versions should be created using LaTeX
and the LIPIcs style file (put \def\copyrightline{} before \begin{document}).
Registration, Travel
joint FOPARA+WST online registration
Participants are expected to arrive on August 28th evening,
and indeed the bus to Bertinoro will leave Bologna
at around 19.00 that day. So, your flight or train
should arrive at Bologna at 18.30 or before.
The Workshop ends on August 31st afternoon.
The exact schedule for the bus to Bologna is not yet fixed but,
again, participants should book flights or trains
leaving Bologna at 17.00 or after.
In the 17.00-19.00 slots there are many flights to-from European cities
(Amsterdam, Paris, Frankfurt, Munich, London, Madrid, etc).
Johannes Waldmann
| Fakultät IMN
| HTWK Leipzig