ABSTRACT. In Bound Analysis we are given a program and we seek functions that bound the growth of computed values, the running time, etc., in terms of input parameters. Problems of this type are uncomputable for ordinary, full languages, but may be solvable for weak languages, possibly representing an abstraction of a "real" program. In 2008, Jones, Kristiansen and I showed that, for a weak but non-trivial imperative programming language, it is possible to decide whether values are polynomially bounded. In this talk, I will focus on current work with Geoff Hamilton, where we show how to compute tight polynomial bounds (up to constant factors) for the same language. We have been able to do that as efficiently as possible, in the sense that our solution has polynomial space complexity, and we showed the problem to be PSPACE-hard. The analysis is a kind of abstract interpreter which computes in a domain of symbolic bounds plus just enough information about data-flow to correctly analyse loops. A salient point is how we solved the problem for multivariate bounds through the intermediary of univariate bounds. Another one is that the algorithm looks for worst-case lower bounds, but a completeness result shows that the maximum of these lower-bound functions is also an upper bound (up to a constant factor).

ABSTRACT. We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary-ternary representations of positive integers. Termination of this rewriting system is equivalent to the Collatz conjecture. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses the automated method of matrix/arctic interpretations and we perform experiments where we obtain proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach.

ABSTRACT. We contribute a Scheme program for deVrijer’s proof of strong normalization of the simply-typed lambda calculus.

ABSTRACT. We consider triangular weakly non-linear loops (twn-loops) over subrings S of R_A, where R_A is the set of all real algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. We present a reduction from the question of termination on all inputs to the existential fragment of the first-order theory of S and R_A. For loops over R_A, our reduction entails decidability of termination. For loops over Z and Q, it proves semi-decidability of non-termination. Furthermore, we show that the halting problem, i.e., termination on a given input, is decidable for twn-loops over any subring of R_A . This also allows us to compute witnesses for non-termination. Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f (∥(x 1 , . . . , x d )∥), where ∥ · ∥ denotes the 1-norm. This result implies that the runtime complexity of a terminating triangular linear loop over Z is at most linear.

ABSTRACT. In this paper we prove that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable.

ABSTRACT. Termination analysis of C programs is challenging. On the one hand, the analysis needs to be precise. On the other hand, programs in practice are usually large and require substantial abstraction. In this extended abstract, we sketch an approach for modular symbolic execution to analyze termination of C programs with several functions. This approach is also suitable to handle recursive programs. We implemented it in our automated termination prover AProVE and evaluated its power on recursive and large programs.

ABSTRACT. We present a novel modular approach to infer upper bounds on the expected runtimes of probabilistic integer programs automatically. To this end, it computes bounds on the runtimes of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.

ABSTRACT. In this workshop paper, we revisit the notion of parallel-innermost term rewriting. We provide a definition of parallel complexity and propose techniques to derive upper bounds on this complexity via the Dependency Tuple framework by Noschinski et al.

ABSTRACT. Derivational complexity of term rewriting considers the length of the longest rewrite sequence for arbitrary start terms, whereas runtime complexity restricts start terms to basic terms. Recently, there has been notable progress in automatic inference of upper and lower bounds for runtime complexity. I propose a novel transformation that lets an off-the-shelf tool for inference of upper or lower bounds for runtime complexity determine upper or lower bounds for derivational complexity as well. The approach is applicable to derivational complexity problems for innermost rewriting and for full rewriting. I have implemented the transformation in the tool AProVE and conducted an extensive experimental evaluation. My results indicate that bounds for derivational complexity can now be inferred for rewrite systems that have been out of reach for automated analysis thus far.

ABSTRACT. The formulation and undecidability proof of the *halting problem* is usually attributed to Turing's 1936 landmark paper. In 2004, though, Copeland noticed that it was so named and, apparently, first stated in a 1958 book by Martin Davis. Indeed, in his paper Turing payed no attention to halting machines. Words (or prefixes) like ``halt(ing)'', ``stop'' or ''terminat(e,ing)'' do not occur in the text. Turing partitions his machines into two classes of *non-halting machines*, one of them able to produce the kind of real numbers he was interested in. His notion of computation did not require termination. His decidability results concerned the classification of his machines (*satisfactoriness* problem) and their `productivity' (*printing* problem). No attempt to formulate or prove the halting problem is made. Other researchers were concerned with these issues, though. We briefly discuss their role in formulating what we currently understand as the *halting problem*.

ABSTRACT. We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.

ABSTRACT. In this paper, we consider non-termination in logic programming and in term rewriting and we recall some well-known results for observing it. Then, we instantiate these results to loopingness, a simple form of non-termination. We provide a bunch of examples that seem to indicate that the instantiations are correct as well as partial proofs.

ABSTRACT. In this paper, we are interested in termination analysis of Single-path Linear-Constraint loops (SLC loops) using Multiphase-Linear Ranking Functions (M{\Phi}RFs for short), in particular, in identifying sub-classes of SLC loops for which M{\Phi}RFs are sufficient, i.e., they terminate iff they have M{\Phi}RFs. We prove this result for two kinds of loops: Octagonal relations and Affine relations with the finite-monoid property.