ABSTRACT. Tuple interpretations are a class of algebraic interpretation that subsumes both polynomial and matrix interpretations as it does not impose simple termination and allows non-linear interpretations. It was developed in the context of higher-order rewriting to study derivational complexity of algebraic functional systems. In this short paper, we continue our journey to study the complexity of higher-order TRSs by tailoring tuple interpretations to deal with innermost runtime complexity.

ABSTRACT. The higher-order recursive path ordering is one of the oldest, but still very effective, methods to prove termination of higher-order TRSs. A limitation of this ordering is that it is not transitive (and its transitive closure is not computable). We will present a transitive variation of HORPO. Unlike previous HORPO definitions, this method can be used directly on terms in curried notation.

ABSTRACT. We present a simple method for obtaining automata that over-approximate match-heights for the set of right-hand sides of forward closures of a given string rewrite system. The method starts with an automaton that represents height-indexed copies of right-hand sides, and inserts epsilon transitions only. Rules that have no redex path in the highest level, are relatively match-bounded, and thus terminating relative to the others, on the starting language. For height bound 0, we obtain a generalisation of right barren string rewriting. An implementation of our method proves termination of 590 out of 595 benchmarks in TPDB/SRS_Standard/ICFP_2010 quickly.

ABSTRACT. We encode the Battle of Hercules and Hydra as a rewrite system with AC symbols. Its termination is proved by a new termination criterion for AC rewriting.

ABSTRACT. Recently, a calculus to combine various techniques for loop acceleration in a modular way has been introduced [Frohn, TACAS 2020]. We show how to adapt this calculus for proving non-termination. An empirical evaluation demonstrates the applicability of our approach.

ABSTRACT. In previous work we showed that for so-called triangular weakly non-linear loops over rings S like Z, Q, or R, the question of termination can be reduced to the existential fragment of the first-order theory of S. For loops over R, our reduction implies decidability of termination. For loops over Z and Q, it proves semi-decidability of non-termination. In this paper, we show that there is an important class of linear loops where our decision procedure results in an efficient procedure for termination analysis, i.e., where the parameterized complexity of deciding termination is polynomial.

ABSTRACT. In former work, we developed an approach for automatic complexity analysis of integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts. In this paper, we show how recent techniques to improve automated termination analysis of integer programs (like the generation of multiphase-linear ranking functions and control-flow refinement) can be integrated into our approach for the inference of runtime bounds. Our approach is implemented in the complexity analysis tool KoAT.

ABSTRACT. In former work, we developed an approach for automatic complexity analysis of integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts. Recently, we extended and reimplemented this approach in a new version of our open-source tool KoAT. In order to compute runtime bounds, we analyze subprograms in topological order, i.e., in case of multiple consecutive loops, we start with the first loop and propagate knowledge about the resulting values of variables to subsequent loops. By inferring runtime bounds for one subprogram after the other, in the end we obtain a bound on the runtime complexity of the whole program. We first try to compute runtime bounds for subprograms by means of multiphase linear ranking functions (MRFs). If MRFs do not yield a finite runtime bound for the respective subprogram, then we apply a technique to handle so-called triangular weakly non-linear loops (twn-loops) on the unsolved parts of the subprogram. Moreover, we integrated control-flow refinement via partial evaluation to improve the automatic complexity analysis of programs further. Additionally, we introduced the notion of expected size which allowed us to extend our approach to the computation of upper bounds on the expected runtimes of probabilistic programs.

ABSTRACT. CeTA is a certifier that can be used to validate automatically generated termination and complexity proofs during the termination competition 2022. We briefly highlight some features of CeTA that have been recently added.

ABSTRACT. We describe the Matchbox termination prover that takes part in the category of certified termination of string rewriting in the Termination Competition 2022.