ABSTRACT. We examine specifications for dependence on the agent that performs them. We look at the consequences for the Church-Turing Thesis and for the Halting Problem.

ABSTRACT. The Size-Change Principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types extending LF.

ABSTRACT. In earlier work, we developed approaches for automated termination analysis of several different programming languages, based on back-end techniques for termination proofs of term rewrite systems and integer transition systems. In the last years, we started adapting these approaches in order to analyze the complexity of programs as well. However, up to now a severe drawback was that we assumed the program variables to range over mathematical integers instead of bitvectors. This eases mathematical reasoning but is unsound in general. While we recently showed how to handle fixed-width bitvector integers in termination analysis, we now present the first technique to analyze the runtime complexity of programs with bitvector arithmetic. We implemented our contributions in the tool AProVE and evaluate its power by extensive experiments.

ABSTRACT. We present an extension of the Kachinuki order on strings. The Kachinuki order transforms the problem of comparing strings to the problem of comparing their syllables length-lexicographically, where the syllables are defined via a precedence on the alphabet. Our extension allows the number of syllables to increase under rewriting, provided we bound it by a weakly compatible interpretation.

ABSTRACT. We generalize term rewriting techniques to finite, directed, ordered multigraphs. We define well-founded monotonic graph rewrite orderings inspired by the recursive path ordering on terms. Our graph path ordering provides a building block for rewriting with such graphs, which should impact the many areas in which computations take place on graphs.

ABSTRACT. We consider complexity proofs for rewrite systems that involve matrix interpretations. In order to certify these proofs, we have to validate polynomial bounds on the matrix growth of A^n for some non-negative real-valued square matrix A. Whereas our earlier certification criterion used algebraic number arithmetic in order to compute all maximal Jordan blocks, in this paper we present a Perron-Frobenius like theorem. Based on this theorem it suffices to just compute the Jordan Blocks of eigenvalue 1, which can easily be done. This not only helps to improve the efficiency of our certifier CeTA, but might also be used to actually synthesize suitable matrix interpretations.

ABSTRACT. On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other hand, automation of such checks would save time and help to establish correctness of exam solutions, examples in lecture notes etc. To this end, we introduce a template mechanism for the termination tool TTT2 that allows us to restrict parameters of certain termination methods. In the extreme, when all parameters are fixed, such restrictions result in checks for specific proofs.

ABSTRACT. Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termination analysis seems essential. This is a largely unexplored area of research in termination analysis, where most effort has focused on small but difficult single-procedure problems.

We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show the advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.

ABSTRACT. We prove that operational termination of declarative programs can be characterized by means of well-founded relations between specific formulas which can be obtained from the program. We show how to generate such relations by means of logical models where the interpretation of some binary predicates are required to be well-founded relations. Such logical models can be automatically generated by using existing tools. This provides a basis for the implementation of tools for automatically proving operational termination of declarative programs.

ABSTRACT. We report on our ongoing work on automated verification of rewriting-based query optimizers. Rewriting-based query optimizers are a widely adapted in relational database architecture however, designing these rewrite systems remains a challenge. In this paper, we discuss automated termination analysis of optimizers where rewrite-rules are expressed in a SQL-like programming language called HoTTSQL, for which semantic equivalence is decidable and a rich theory and some tools have been developed. We discuss how it is not sufficient to reason about rule specific (local) properties such as semantic equivalence, and it is necessary to work with set-of-rules specific (global) properties such as termination and loop-freeness to prove correctness of the optimizer. We put forward a way to translate the rules in HoTTSQL and reason termination using Tyrolean Termination Tool 2.

ABSTRACT. In this extended abstract we explored the use of partial evaluation as a control-flow refinement technique in the context for termination and cost analysis. Our preliminary experiments show that partial evaluation can improve both analyses.

ABSTRACT. In this extended abstract, we describe a preliminary work on inferring linear upper-bounds on the expected cost for control-flow graphs as via cost relations, with the goal of integrating this process in the SACO tool, whose cost analyzer is based on the use of cost relations as well.

ABSTRACT. Weight functions are among the simplest methods for proving termination of string rewrite systems, and of rather limited applicability. In this working paper, we propose a generalized approach. As a first step, syllable decomposition yields a transformed, typically infinite rewrite system over an infinite alphabet, as the title indicates. Combined with generalized weight functions, termination proofs become feasible also for systems that are not necessarily simply terminating. The method is limited to systems with linear derivational complexity, however, and this working paper is restricted to original alphabets of size two. The proof principle is almost self-explanatory, and if successful, produces simple proofs with short proof certificates, often even shorter than the problem instance. A prototype implementation was used to produce nontrivial examples.

ABSTRACT. We revisit the static dependency pair method for termination of higher-order term rewriting. In this extended abstract, we generalise the applicability criteria for the method. Moreover, we propose a static dependency pair framework based on an extended notion of computable dependency chains that harnesses the computability-based reasoning used in the soundness proof of static dependency pairs. This allows us to propose a new termination proving technique to use in combination with static dependency pairs: the static subterm criterion.