ABSTRACT. The question of how to ensure that programs terminate has been for decades attracting remarkable attention of computer scientists, resulting in a great number of techniques for proving termination of term rewriting and other models of computation. Nowadays it has become hard for new-comers to come up with new termination techniques/tools, since there are so many to learn/implement before inventing a new one. In this talk, I present my past and on-going works towards unified method for termination, that allow one to learn/implement a single idea and obtain many well-known techniques as instances.

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 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. 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. 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. 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 HoTTSQL. 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 to Term Rewriting Systems, opening avenues for the use of termination tools in the analysis of rewriting-based transformations of HoTTSQL database queries. 

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. 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. 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.