List of Papers

Preliminary Program

Timing for the talks: basic interval is 30 minutes (this includes presentation, discussion, and changing computers for the next speaker). Each session has two or three intervals. Coffee break (between Sessions 1/2, resp. 3/4) is one interval. Morning session starts at 9 a.m., lunch break is 12:30 - 2 p.m., last session ends 5 p.m.

Tuesday, June 2nd

7 p.m. informal get-together at restaurant Gosenschenke, location

Wednesday, June 3rd

Session 1 (Keynote Talk)

The SMT* Platform: Design, Implementation, and Experience.

Morgan Deters 

Session 2

 Polynomial constraint solving using SMT

Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodriguez-Carbonell, Albert Rubio

 CeTA - A Tool for Certified Termination Analysis

 Christian Sternagel, Rene Thiemann, Sarah Winkler, Harald Zankl

Non-Collapsing Context-Sensitive Dependency Pairs

 Beatriz Alarcon, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raul Gutierrez, Salvador Lucas, Peter Schneider-Kamp, Rene Thiemann

Mechanizing Proofs of Termination with Context-Sensitive Dependency Pairs

 Raul Gutierrez, Salvador Lucas

Lunch

 

Session 3

On Some Implementation Aspects of VMTL

 Felix Schernhammer, Bernhard Gramlich

Termination Analysis of Java Bytecode by Term Rewriting

 Carsten Otto, Marc Brockschmidt, Christian von Essen, Jürgen Giesl

Termination of Integer Term Rewriting

 Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, Stephan Falke

Session 4

The Termination Competition Execution Platform

Simon Bailey, Michael Weber

Meeting of the Termination Competition Steering Committee

for agenda, see http://termination-portal.org/wiki/TC_SC_Meeting_WST09

Reception

at workshop location, Mediencampus

 

Thursday, June 4th

Session 1

Combinatorial Problems by Termination of Rewriting

Hans Zantema

Derivational complexity of {aa -> bc, bb -> ac, cc -> ab}

 Karel Chvalovsky

The Subterm Criterion in Complexity Analysis

 Nao Hirokawa, Georg Moser

Session 2

A new approach to non-termination analysis of Logic Programs

 Dean Voets, Daniel De Schreye

Deciding Loops under Strategies

 Rene Thiemann, Christian Sternagel

System Description: KnockedForLoops

Dieter Hofbauer 

Lunch

 

Session 3

Monotonicity of Parametric Polynomials

 Friedrich Neurauter

Matrix interpretations revisited

 Pierre Courtieu, Gladys Gbedo, Olivier Pons

Proving Termination with Matrix Interpretations over the Reals

 Beatriz Alarcon, Salvador Lucas, Rafael Navarro-Marset

Session 4

Equational Reasoning for Termination of Rewriting

 Harald Zankl, Aart Middeldorp

Inductive Theorem Proving meets Dependency Pairs

 Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp

Dinner

 at restaurant Stelzenhaus, location

Friday, June 5th

Session 1

Proving Termination of Programs with Second-Order Recursion

 Markus Aderhold

Checking the Influence of Non-Termination on Free Theorems

 Daniel Seidel, Janis Voigtländer

Getting to the _|_

 Jan Christiansen

Session 2

Proving Termination for Logic Programs with Cut

 Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, Thomas Ströder, Rene Thiemann

Proving termination by invariance relations

 Paolo Pilozzi, Daniel De Schreye

A Mechanized Proof Reconstruction for SCNP Termination

 Alexander Krauss, Armin Heller

Lunch

 

Session 3

Type Systems for the Termination of Mobile Processes

 Romain Demangeon

Polynomial Path Orders and the Rules of Predicative Recursion with Parameter Substitution

 Martin Avanzini, Georg Moser

Beyond Dependency Graphs

 Martin Korp, Aart Middeldorp

Report on the Termination Competition 2008

 Johannes Waldmann (editor)