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.

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.

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.

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.