|Friday, April 22
If you have any questions regarding the organization of the meeting, please contact:
| Friday, April 29
|Non-Termination by Finite Automata
|Jörg Endrullis, Vrije Universiteit Amsterdam
|Loop Detection for Lower Runtime Bounds
|Florian Frohn, RWTH Aachen
|Term Graph Rewriting
|Hans Zantema, TU Eindhoven / RU Nijmegen
|Verifying Procedural Programs via Constrained Rewriting Induction
|Carsten Fuhs, Birkbeck, University of London
|TeReSe business meeting
|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.
|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.