20th Informal Workshop on Term Rewriting

April 29, 2016         Aachen, Germany

Important Dates - Practical Information - Preliminary Schedule - Abstracts

The TeReSe meetings started with a festive meeting in Amsterdam celebrating the publication of the TeReSe book. Traditionally, the format of this meeting is an afternoon of presentations with room for discussions over dinner. Subsequent workshops took place in Eindhoven, in Utrecht, in Eindhoven, in Aachen, in Amsterdam, in Utrecht, in Eindhoven, in Aachen, in Amsterdam, in Nijmegen, in Utrecht, in Aachen, in Amsterdam, in Eindhoven, in Utrecht, in Aachen, in Amsterdam, and in Nijmegen. We hope to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research.


Participant registrationFriday, April 22

Please contact Jera Hensel for registering participants.


The TeReSe will take place in the computer science complex located at Ahornstr. 55. The presentations will be held in the seminar room 4201b of "Lehrstuhl Informatik 2", which is located on the second floor of building E1. For information on how to get there, please look at the arrival information.

If you have any questions regarding the organization of the meeting, please contact:

Jera Hensel

PRELIMINARY SCHEDULE  (Ahornstr. 55, Building E1, Seminar room 4201b of "Lehrstuhl Informatik 2")

Friday, April 29

14:00 - 14:45   Non-Termination by Finite Automata

Jörg Endrullis, Vrije Universiteit Amsterdam
14:45 - 15:30   Loop Detection for Lower Runtime Bounds

Florian Frohn, RWTH Aachen
15:30 - 16:00   Coffee Break
16:00 - 16:45   Term Graph Rewriting

Hans Zantema, TU Eindhoven / RU Nijmegen
16:45 - 17:30   Verifying Procedural Programs via Constrained Rewriting Induction

Carsten Fuhs, Birkbeck, University of London
17:30 - 17:45   TeReSe business meeting

18:15 - ??:??   Dinner at Sen (Theaterstr. 27) - location info


Jörg Endrullis: Non-Termination by Finite Automata

We present a technique for proving looping and non-looping non-termination of term rewriting. Our technique employs finite automata to describe a regular tree language such that every term in the language permits some rewrite step to a term in the language. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic. If time permits, we will discuss an extension to non-termination of cycle rewriting.

Florian Frohn: Loop Detection for Lower Runtime Bounds

We present a new approach to deduce lower bounds for (worst-case) runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing methods that compute upper complexity bounds. The presented loop detection technique searches for "decreasing loops". Decreasing loops generalize the notion of loops for TRSs, and allow us to detect families of rewrite sequences with linear, exponential, or infinite length. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.

Hans Zantema: Term Graph Rewriting

After an introduction to term graphs we will present two natural ways to apply term rewrite rules on term graphs, and show the difference. We will show how for both flavors we can automatically prove termination of the resulting term graph rewrite systems by transforming them to graph transformation systems and applying the termination tool we developed for that.

This is joined work with Dennis Nolte and Barbara Koenig from Duisburg.

Carsten Fuhs: Verifying Procedural Programs via Constrained Rewriting Induction

We aim at developing a verification method for procedural programs via a transformation into the recently introduced Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we introduce an extension of transformation methods based on integer TRSs, which can also handle global variables and arrays as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions, involving for instance integers and arrays. Our approach proves equivalence between two implementations, so in contrast to other works, we do not require an explicit specification in a separate specification language.

This talk is based on joint work with Cynthia Kop and Naoki Nishida.