This paper describes the second edition of the Tyrolean Termination Tool—a fully automatic
termination analyzer for first-order term rewrite systems. The main features of this tool are its …

In this paper, we present a variant of the dependency pair method for analysing runtime
complexities of term rewrite systems automatically. This method is easy to implement, but …

We present a modular framework to analyze the innermost runtime complexity of term
rewrite systems automatically. Our method is based on the dependency pair framework for …

In this paper we present a combination framework for the automated polynomial complexity
analysis of term rewrite systems. The framework covers both derivational and runtime …

In automated complexity analysis of term rewriting, estimating the growth rate of the values
in the k-th power of a matrix A–for fixed A and increasing k–is of fundamental interest. This …

In earlier work, we have shown that for confluent TRSs, innermost polynomial runtime
complexity induces polytime computability of the functions defined. In this paper, we …

Context-sensitive rewriting is a restriction of term rewriting which is obtained by imposing
replacement restrictions on the arguments of function symbols. It has proven useful to …

We develop a class of algebraic interpretations for many-sorted and higher-order term
rewriting systems that takes type information into account. Specifically, base-type terms are …

Higher-order rewriting is a framework in which higher-order programs can be described by
transformation rules on expressions. A computation occurs by transforming an expression …

Abstract The Tyrolean Complexity Tool, TCT for short, is an open source complexity analyser
for term rewrite systems. Our tool TCT features a majority of the known techniques for the …