ABSTRACT. In this talk, we will present and discuss the results of the international termination and complexity competition.

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. LoAT is a tool for proving non-termination and lower bounds on the worst-case complexity of integer transition systems, i.e., programs operating on integers. It supports a variety of input formats, user-defined cost models, and it provides detailed proofs. LoAT is based on loop acceleration, a technique to transform single-path loops into non-deterministic straight-line code. Due to its ability to accelerate loops, LoAT can transform programs with complex control flow into quantifier-free first-order formulas, which can then be analyzed by off-the-shelf SMT solvers.

ABSTRACT. AProVE is a tool for automatic termination and complexity proofs of Java, C, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level languages, AProVE automatically converts them into TRSs and/or Integer Transition Systems (ITSs). Then, a wide range of techniques is employed to prove termination and to compute complexity bounds for the resulting TRSs or ITSs. In particular, the tools KoAT and LoAT are used to infer upper and lower complexity bounds for ITSs, and LoAT and T2 are used for non-termination proofs of ITSs. For term rewrite systems, the generated proofs can be exported to check their correctness using automatic certifiers. AProVE can easily be used via its web interface and there is also a corresponding plug-in for the popular Eclipse software development environment.

ABSTRACT. SOL is a Haskell-based tool for showing confluence and strong normalisation of higher-order computation rules. Termination analysis is based on Blanqui's General Schema criterion and a new modular termination proof method of second-order computation systems recently shown by Hamana.

ABSTRACT. In this short presentation, I will discuss the tool WANDA (a participant in the higher-order termination category of the termination competition). In particular, I will focus on weaknesses of WANDA, and challenges where other participants have something to win!

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.

ABSTRACT. The software tool MultumNonMulta (MnM) aims at proving termination or non-termination of string rewrite systems automatically. The purpose of this prototype implementation is to demonstrate the power of a combination of few but strong proof methods, notably matrix interpretations. After a short survey of old and new features, we discuss the reasons that prevent MnM from taking part in the certified categories of the termination competition.

ABSTRACT. Thus far, the annual Termination and Complexity Competition (TermComp) has focussed on analysis of sequential languages. We aim to broaden the scope of TermComp to languages with parallel computation. As a first step, we consider (max-)parallel-innermost term rewriting. In contrast to innermost rewriting, which rewrites only one innermost redex at a time, parallel-innermost rewriting uses a multi-step rewrite relation: all innermost redexes are rewritten simultaneously. This approach can lead to significant decreases in the maximal length of the rewrite sequence from a given term when compared to innermost rewriting.

In this talk, we present a new category proposal for runtime complexity of parallel-innermost term rewriting at TermComp. We also discuss recent results on automated analysis techniques for this problem and present experimental results obtained with an implementation of these techniques in the program analysis tool AProVE.

ABSTRACT. We present a simple tool that implements the encodings of Hilbert's 10th problem as (incremental) polynomial termination problems of our FSCD 2022 paper. The tool can be used to generate problems for TPDB, in particular for testing the implementation of polynomial interpretations in termination tools.