ABSTRACT. Automating semantic labelling for termination proofs is a combinatorially hard problem since the number of algebras grows prohibitively large even for small domains. We report on experiments with our tools Matchbox and MnM, comparing various model-finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras.

ABSTRACT. It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. As a corollary, we establish that termination and innermost termination coincide for the class of right-linear overlay TRSs.

ABSTRACT. Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also discuss the use of it as ground total reduction orders.

ABSTRACT. Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for termination analysis and complexity analysis of term rewrite systems. Finding such polynomial interpretations for a given set of term constraints involves solving a set of $\exists\forall$ inequalities over the natural numbers. Conventionally, the absolute positiveness criterion is used to reduce $\exists\forall$ inequalities to $\exists$ inequalities. This extended abstract reports on work in progress to go beyond absolute positiveness, allowing for finding non-linear polynomial interpretations that were outside the reach of existing techniques.

ABSTRACT. Proving termination or non-termination of lasso programs is a challenging problem in program verification. To unify state-of-the-art approaches under a common execution framework, we present PaSTTeL, a modular and generic parallel portfolio framework for termination and non-termination analysis of lasso programs. PaSTTeL is designed to: (1) facilitate the integration of new analysis algorithms into the portfolio, (2) execute registered strategies concurrently, and (3) act as a self-contained library component that can be seamlessly embedded into any external project requiring (non-)termination analysis. Initial experiments demonstrate that an instantiation of PaSTTeL performs competitively against state-of-the-art tools.

ABSTRACT. Linear-constrained loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constrained loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences – integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that ter- mination of one-variable linear-constrained loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.

ABSTRACT. We consider linear single-path loops of the form while φ do x ← Ax + b where x is a vector of variables, the loop guard φ is a conjunction of linear inequations over the variables x, and the update of the loop is represented by the matrix A and the vector b. It is already known that termination of such loops is decidable. In this work, we consider loops where A has real eigenvalues, and prove that it is decidable whether the loop's runtime (for all inputs) is bounded by a constant if the variables range over R or Q. This is an important problem in automatic program verification, since safety of linear while-programs is decidable if all loops have constant runtime, and it is closely connected to the existence of multiphase-linear ranking functions, which are often used for termination and complexity analysis. To evaluate its practical applicability, we also present an implementation of our decision procedure.

ABSTRACT. In this talk, we present the first dependency pair framework for analyzing expected complexity and for proving positive or strong almost-sure termination (SAST) of innermost rewriting with probabilistic term rewrite systems (PTRSs). We implemented our framework in the tool AProVE and demonstrate its power compared to existing techniques for proving SAST.

ABSTRACT. We show that there is a simple syntactically-defined subclass of higher-order benchmarks in the termination problem database for which rewriting according to Nipkow's higher-order rewrite systems (HRSs) and rewriting according to a beta-first strategy in the semantics of TermComp's higher-order category coincide. This lays the formal foundation for an HRS (sub)category in TermComp which would allow more tools to compete against each other.

ABSTRACT. We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Gödel's system T. For terms that can be typed in this system, we define the Global Trace Condition (GTC), adapting the concept from Brotherston and Simpson's Cyclic Proofs, and show that any infinite reduction of a well-typed term satisfying the GTC is strongly convergent. As a corollary, we obtain the proof that any closed term of type Nat reduces to some numeral through any reduction by levels. We argue that the Church-Rosser theorem holds in the limit for our calculus and that the normal forms of closed terms of type N (nat) are unique numerals.

ABSTRACT. In earlier work we introduced a modular framework for computing upper bounds on expected runtimes of randomized programs by combining upper bounds on expected runtime and size complexities of parts of the program. This approach relies only on bounds for expectations, thereby discarding crucial information on the shape of the underlying distributions. This limits the ways in which such bounds can be combined. Hence, our approach often required the consideration of bounds obtained from a classical analysis, where all probabilistic behavior is over-approximated into non-deterministic (non-probabilistic) choice. We now extend this framework by also computing bounds on higher moments. We show how to obtain such bounds for parts of the program by slightly adapting our notion of probabilistic linear ranking functions. This allows for combinations of bounds on expected time and size complexities using Hölder's inequality. So in this way, we can avoid over-approximations using classical bounds, which results in a substantially more powerful approach.

ABSTRACT. We show that existing tools for termination analysis are extremely well suited for LTL model checking of infinite state systems. To this end, we present a framework MoAT which uses the well-known automata-based approach and reduces the LTL model checking problem to deciding fair termination. To prove or disprove fair termination, it then calls the termination tools KoAT and LoAT in the backend. Our experiments show that in this way, MoAT is on par with existing state-of-the-art tools for LTL model checking of infinite state systems.

ABSTRACT. We present the theory underpinning a complexity analysis tool (currently under development) that aims to automate tedious parts of the analysis of complex algorithms originating in the field of automated reasoning. Examples are given by super-exponential quantifier elimination procedures in real and integer arithmetic. Our tool implements the following pipeline: 1. Together with the algorithm to be analysed, the user (an expert, e.g. the algorithm designer) can provide key metrics to track and lemmas to guide and improve the analysis. In pen-and-paper proofs, these correspond to the "non-tedious" and "creative" parts of the complexity analysis, that require human ingenuity. 2. The second step consists in the extraction of (generalised) recurrence equations. Here, we rely on a novel higher-order abstract interpretation technique, based on operator semantics. It enables (optimal) abstract compilation of symbolic programs into different kinds of purely numerical recursive representations, such as recurrence equations on interval-valued functions or numerical logic programs. 3. Finally, our tool solves the recurrence equations. We propose going beyond the direct use of computer algebra systems (CAS) by employing pre/postfixpoint-based techniques to discover and verify candidate bounds on the solutions. This approach, in turn, leverages recent progress in SMT solvers, and could benefit from techniques originating in termination-analysis research.