WST  2004

7th International Workshop on Termination


June 1 - 2, 2004          Aachen, Germany



Tentative Program - Topics - Submission - Dates - Program Committee - Local Arrangements


After the successful workshops held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), and Valencia (2003), the 7th International Workshop on Termination will be held in Aachen. We hope to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research and subsequent publications.

PROGRAM  (Karman-Auditorium, Lecture Hall Fo 4)

Tuesday June 1

9:30 - 10:00   Erasure and Termination in Higher-Order Rewriting




J. Ketema, F. van Raamsdonk
10:00 - 10:30   Reducing the Constraints of the Dependency Pair Approach




J. Giesl, R. Thiemann, P. Schneider-Kamp
 
10:30 - 11:15   Coffee Break
 
11:15 - 11:45   Report on the Termination Competition




C. Marché
11:45 - 12:15   MU-TERM: A Tool for Proving Termination of Rewriting with Replacement Restrictions




S. Lucas
 
12:15 - 14:00   Lunch
 
14:00 - 15:00   Invited Talk




Danny de Schreye
15:00 - 15:30   Abstract Partial Evaluation for Termination Analysis




L. Tamary, M. Codish
 
15:30 - 16:15   Coffee Break
 
16:15 - 16:45   Polynomials over the Reals in Proofs of Termination




S. Lucas
16:45 - 17:15   Natural Polynomial Interpretations




N. Hirokawa, A. Middeldorp

Wednesday June 2

9:00 - 9:30   Modularity of Termination of Left-Linear Rewrite Systems Revisited




B. Gramlich
9:30 - 10:00   A Note on a Term Rewriting Characterization of PTIME




T. Arai, G. Moser
10:00 - 10:30   A Practical Approach to Proving Termination of Recursive Programs in Theorema




N. Popov, T. Jebelean
 
10:30 - 11:00   Coffee Break
 
11:00 - 11:30   Proof-Theoretic Analysis of Lexicographic Path Orders




J.W. Klop, V. van Oostrom, R. de Vrijer
11:30 - 12:00   Tree Automata that Certify Termination of Term Rewriting Systems




A. Geser, D. Hofbauer, J. Waldmann, H. Zantema
12:00 - 12:30   Relative Termination in Term Rewriting




H. Zantema
 
12:30 - 14:00   Lunch
 
14:00 - 14:30   Proving termination with AProVE




J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke
14:30 - 15:00   Tyrolean Termination Tool




N. Hirokawa, A. Middeldorp
15:00 - 15:30   Connecting Remote Termination Tools




M. Alpuente, S. Lucas
 
15:30 - 16:00   Coffee Break
 
16:00 - 18:00   Demo/Exhibition of Termination Tools
This event takes place in Room SFo 1


TOPICS

This workshop delves into all aspects of termination of processes. Though the halting of computer programs is undecidable, methods of establishing termination play a fundamental role in many applications and the challenges are both practical and theoretical. From a practical point of view, proving termination is a central problem in software development and formal methods for termination analysis are essential for program verification. From a theoretical point of view, termination is central in mathematical logic and ordinal theory.

Areas of interest to this workshop, include, but are not limited to, the following: Following the success at last year's workhop, apart from the presentation sessions there will be an exhibition/competition of termination provers.

SUBMISSION

Extended abstracts of at most 4 pages in the official RDP 2004 workshop format (see below) should be submitted electronically (PS or PDF) to wst04@cs.bgu.ac.il. The proceedings of WST 2004 will be published as a technical report of the Computer Science Department of RWTH Aachen. Authors are requested to use the RDP 2004 workshop style file.

DATES

Submission Deadline:    March 17, 2004
Notification: April 9, 2004
Final Version: April 30, 2004

PROGRAM COMMITTEE

Michael Codish Beer-Sheva co-chair
Danny De Schreye Leuven
Alfons Geser Hampton, VA
Neil D. Jones Copenhagen  
Claude Marché Orsay
Aart Middeldorp Innsbruck co-chair
Frederic Mesnard La Réunion
Helmut Schwichtenberg   Munich
Harald Søndergaard Melbourne

EXHIBITION / COMPETITION

Claude Marché   Orsay
Albert Rubio Barcelona

LOCAL ARRANGEMENTS

Jürgen Giesl
RWTH Aachen, Germany
giesl@informatik.rwth-aachen.de