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