List of accepted papers

Conrad Rau, David Sabel and Manfred Schmidt-Schauss
Encoding Induction in Correctness Proofs of Program Transformations as a Termination Problem
Abstract: The diagram-based method to prove correctness of program transformations consists of computing complete set of (forking and commuting) diagrams, acting on sequences of standard reductions and program transformations. In many cases, the only missing step for proving correctness of a program transformation is to show the termination of the rearrangement of the sequences. Therefore we encode complete sets of diagrams as term rewriting systems and use an automated tool to show termination, which provides a further step in the automation of the inductive step in correctness proofs.

Bernhard Gramlich and Klaus Györgyfalvay
On Modularity of Termination Properties of Rewriting under Strategies
Abstract: The modularity of termination and confluence properties of term rewriting systems has been extensively studied, for disjoint unions and other more types of combinations. However, for rewriting under strategies the theory is less well explored. Here we extend the modularity analysis of termination properties systematically to (variants of) innermost and outermost rewriting. It turns out — as expected — that in essence innermost rewriting behaves nicely w.r.t. modularity of termination properties, whereas this is not all the case for outermost rewriting, at least not without further assumptions.

Christian Sternagel and René Thiemann
A Relative Dependency Pair Framework
Abstract: We present a relative DP framework which generalizes the existing DP framework by allowing weak pairs and strict rules and forms the basis of our proof checker CeTA. The new framework can be used to characterize relative termination using dependency pairs. One of its main features is the possibility to split a DP problem into two DP problems which can be treated independently. By such a split we can easily solve problems that arise when using incomplete termination techniques or techniques like unlabeling which revert the effect of earlier techniques.

Marc Brockschmidt, Thomas Ströder, Carsten Otto and Jürgen Giesl
Proving Non-Termination for Java Bytecode
Abstract: Recently, we developed an approach for automated termination proofs of Java Bytecode (JBC), which is based on constructing and analyzing termination graphs. These graphs represent all possible program executions in a finite way. In this paper, we show that this approach can also be used to detect non-termination. We implemented our results in the termination prover AProVE and provide experimental evidence for the power of our approach.

Harald Zankl, Sarah Winkler, Aart Middeldorpt
Automating Ordinal Interpretations
Abstract: In this note we study weakly monotone interpretations for direct proofs of termination which is sound if the interpretation functions are ``simple''. This is e.g. the case for standard addition and multiplication of ordinal numbers. We compare the power of such interpretations to polynomial interpretations over the natural numbers and report on preliminary experimental results.

Fabian Emmes, Tim Enger and Jürgen Giesl
Detecting Non-Looping Non-Termination
Abstract: We introduce a technique to prove non-termination of term rewrite systems automatically. In contrast to most previous approaches, our technique is also able to detect non-looping nontermination.

René Thiemann
A Report on the Certification Problem Format
Abstract: We show how the certification problem format is beneficial for certification of termination proofs. We further highlight some of its design decisions and mention problems that are open for discussion.

Alexander Bau, Tobias Kalbitz, Maria Voigtländer and Johannes Waldmann
Recent Developments in the Matchbox Termination Prover
Abstract: We report on recent and ongoing work on the Matchbox termination prover: a constraint compiler that transforms a Boolean-valued Haskell function into a Boolean satisfiability problem (SAT),a constraint solver for real and arctic matrix constraints that is using evolutionary optimization, and is running on massively parallel (graphics) hardware.

Martin Avanzini, Naohi Eguchi and Georg Moser
On a Correspondence between Predicative Recursion and Register Machines
Abstract: We present the small polynomial path order sPOP*. Based on sPOP*, we study a class of rewrite systems, dubbed systems of predicative recursion of degree d, such that for rewrite systems in this class we obtain that the runtime complexity lies in O(n^d). We show that predicative recursive rewrite systems of degree d define functions computable on a register machine in time O(n^d).

Cristina Borralleras, Miquel Bofill, Enric Rodríguez Carbonell and Albert Rubio
The recursive path and polynomial ordering
Abstract: In most termination tools two ingredients, namely recursive path orderings (RPO) and polynomial interpretation orderings (POLO), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. We present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extends them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatment for the others. The ordering is extended to higher-order terms, providing an automatable use of polynomial interpretations in combination with beta-reduction.

Michael Codish, Igor Gonopolskiy, Amir Ben-Amram, Carsten Fuhs and Jürgen Giesl
Termination Analysis via Monotonicity Constraints over the Integers and SAT Solving
Abstract: We describe an approach for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a non-trivial extension of the size-change termination method. In this setting, termination is PSPACE complete, hence we focus on a significant subset in NP, which we call MCNP, designed to be amenable to a SAT-based solution. We use ranking functions in terms of bounded differences between multisets of integers. Experiments with our approach as a back-end for termination analysis of Java Bytecode with AProVE and COSTA as front-ends reveal a good trade-off between precision and cost of analysis.

Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
Proving Termination of Java Bytecode with Cyclic Data
Abstract: In earlier work, we developed a technique to prove termination of Java Bytecode (JBC) automatically: first, JBC programs are automatically transformed to term rewrite systems (TRSs) and then, existing methods and tools are used to prove termination of the resulting TRSs. In this paper, we extend our technique in order to prove termination of algorithms on cyclic data such as cyclic lists or graphs automatically. We implemented our technique in the tool AProVE and performed extensive experiments to evaluate its practical applicability.

Patrick Baillot and Ugo Dal Lago
Higher-Order Interpretations and Program Complexity
Abstract: Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. Here we extend this approach to the higher-order setting. For that we consider the notion of simply typed term rewriting systems, we define higher-order polynomial interpretations (HOPI) for them and give a criterion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is flexible enough to validate some interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations,coupled with a simple termination criterion based on linear types and path-like orders.

Beniamino Accattoli and Ugo Dal Lago
On the Invariance of Derivational Complexity for Head Reduction
Abstract: The lambda-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, derivational complexity is indeed a reasonable cost model. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies derivation complexity is an invariant cost model, if any.

Bertram Felgenhauer
Binomial Interpretations
Abstract: Polynomial interpretations can be used for proving termination of term rewrite systems. In this note, we contemplate binomial interpretations based on binomial coefficients, and show that they form a suitable basis for obtaining (weakly) monotone algebras. The main motivation is that this representation covers examples with negative coefficients like f(x) = 2x² - x + 1, and even some polynomials with rational coefficients like f(x) = x(x-1)/2 that map natural numbers to natural numbers.

Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp and Jürgen Giesl
Automated Runtime Complexity Analysis for Prolog by Term Rewriting
Abstract: For term rewrite systems (TRSs), a huge number of automated termination analysis techniques have been developed during the last decades, and by automated transformations of Prolog programs to TRSs, these techniques can also be used to prove termination of Prolog programs. Very recently, techniques for automated termination analysis of TRSs have been adapted to prove asymptotic upper bounds for the runtime complexity of TRSs automatically. In this paper, we present ongoing work to transform Prolog programs automatically into TRSs in such a way that the resulting TRSs have at least the same asymptotic upper complexity bound. Thus, techniques for complexity analysis of TRSs can be applied to prove upper complexity bounds for Prolog programs.

Georg Moser and Michael Schaper
Termination Graphs Revisited
Abstract: We revisit termination graphs from the viewpoint of runtime complexity. Suitably generalising the construction proposed in the literature, we define an alternative representation of JBC executions as computation graphs. We show that the transformation from JBC programs to computation graphs is sound, that is termination preserving. Moreover, we establish that the transformation is complexity preserving.

Friedrich Neurauter and Aart Middeldorp
Matrix Interpretations for Polynomial Derivational Complexity
Abstract: Matrix interpretations can be used to bound the derivational complexity of term rewrite systems. In general, the obtained bounds are exponential. In this paper we use joint spectral radius theory in order to completely characterize matrix interpretations that induce polynomial upper bounds on the derivational complexity of (compatible) rewrite systems.