About Conferences Colloquium Workshops Practical

WST 2007 Programme



Friday, June 29


8:15 - 9:00      Arrival of participants and registration

       WST Session 1: Matrices and Dependency Pairs (Room 35-2-25)
9:00 - 9:15      Johannes Waldmann. Arctic Termination.
9:15 - 9:30      Andreas Gebhardt, Dieter Hofbauer and Johannes Waldmann. Matrix Evolutions.
9:30 - 9:45      Adam Koprowski and Hans Zantema. Certification of Matrix Interpretations in Coq.
9:45 - 10:00      Jürgen Giesl, René Thiemann, Stephan Swiderski and Peter Schneider-Kamp. Termination of TRSs with Bounded Increase.
10:00 - 10:15      Jörg Endrullis and Jeroen Ketema. Root Stabilisation Using Dependency Pairs.
10:15 - 10:30      Beatriz Alarcón, Raúl Gutiérrez and Salvador Lucas. Improving Termination Proofs of Context-Sensitive Rewriting using Dependency Pairs.

10:30 - 11:00      Coffee Break

       WST Session 2: Programming languages (Room 35-2-25)
11:00 - 11:15      Dean Voets, Paolo Pilozzi and Danny De Schreye. A new approach to termination analysis of Constraint Handling Rules.
11:15 - 11:30      Paolo Pilozzi, Tom Schrijvers and Danny De Schreye. Proving termination of CHR in Prolog: A transformational approach.
11:30 - 11:45      Amir Ben-Amram and Chin Soon Lee. Ranking Functions for Size-Change Termination II.
11:45 - 12:00      Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, German Puebla and Damiano Zanardini. Termination Analysis of Java Bytecode.
12:00 - 12:15      Keiko Nakata and Jacques Garrigue. Path resolution for recursive nested modules is undecidable.
12:15 - 12:30      Nikolaj Popov and Tudor Jebelean. Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema.

12:30 - 14:00      Lunch

       WST Session 3: Satisfiability and Constraint Solving (Room 35-2-25)
14:00 - 14:15      Harald Zankl and Aart Middeldorp. Nontermination of String Rewriting using SAT.
14:15 - 14:30      Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish and Jürgen Giesl. Implementing RPO using SAT.
14:30 - 14:45      Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann and Harald Zankl. SAT Solving for Termination Analysis with Polynomial Interpretations.
14:45 - 15:00      Salvador Lucas. Solving polynomial constraints over the reals in proofs of termination.
15:00 - 15:15      Salvador Lucas and Rafael Navarro. Fast SAT-based polynomial constraint solving for termination tools.
15:15 - 15:30      Claude Marché, Johannes Waldmann, Hans Zantema. The Termination Competition 2007.

15:30 - 16:00      Coffee Break

       WST Session 4: Conditional Rewriting and Proof Calculi (Room 35-2-25)
16:00 - 16:15      Naoki Nishida, Masahiko Sakai and Terutoshi Kato. Convergent Term Rewriting Systems for Inverse Computation of Injective Functions.
16:15 - 16:30      Felix Schernhammer and Bernhard Gramlich. On Proving and Characterizing Operational Termination of Deterministic Conditional Rewrite Systems.
16:30 - 16:45      Daniel Dougherty, Silvia Ghilezan and Pierre Lescanne. A General Technique for Analyzing Termination in Symmetric Proof Calculi.
16:45 - 17:00      James Brotherston, Richard Bornat and Cristiano Calcagno. A Cyclic Termination Proof of In-Place List Reversal using Separation Logic.
17:00 - 17:30      WST business meeting.

webmaster at rdp07 dot org