next day
all days

View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 120L
Location: Ullmann 309
Tuple Interpretations and Applications to Higher-Order Runtime Complexity
PRESENTER: Deivid Vale

ABSTRACT. Tuple interpretations are a class of algebraic interpretation that subsumes both polynomial and matrix interpretations as it does not impose simple termination and allows non-linear interpretations. It was developed in the context of higher-order rewriting to study derivational complexity of algebraic functional systems. In this short paper, we continue our journey to study the complexity of higher-order TRSs by tailoring tuple interpretations to deal with innermost runtime complexity.

A transitive HORPO for curried systems

ABSTRACT. The higher-order recursive path ordering is one of the oldest, but still very effective, methods to prove termination of higher-order TRSs. A limitation of this ordering is that it is not transitive (and its transitive closure is not computable). We will present a transitive variation of HORPO. Unlike previous HORPO definitions, this method can be used directly on terms in curried notation.

Approximating Relative Match-Bounds
PRESENTER: Dieter Hofbauer

ABSTRACT. We present a simple method for obtaining automata that over-approximate match-heights for the set of right-hand sides of forward closures of a given string rewrite system. The method starts with an automaton that represents height-indexed copies of right-hand sides, and inserts epsilon transitions only. Rules that have no redex path in the highest level, are relatively match-bounded, and thus terminating relative to the others, on the starting language. For height bound 0, we obtain a generalisation of right barren string rewriting. An implementation of our method proves termination of 590 out of 595 benchmarks in TPDB/SRS_Standard/ICFP_2010 quickly.

10:30-11:00Coffee Break
11:00-12:30 Session 125R
Location: Ullmann 309
CeTA — Efficient Certification of Termination Proofs

ABSTRACT. We present recent developments in CeTA w.r.t. the efficient certification of termination proofs. Here, efficiency is seen under various aspects. First, we present a case study on minimizing the formalization effort, namely when trying to verify the classical path orders by viewing them as instances of the weighted path order. Second, we argue that the efficient generation of certificates within termination tools requires more powerful certifiers, in particular when considering the usage of SAT- or SMT-solvers. Third, we present recent developments which aim at improving the execution time of CeTA.

Hydra Battles and AC Termination
PRESENTER: Aart Middeldorp

ABSTRACT. We encode the Battle of Hercules and Hydra as a rewrite system with AC symbols. Its termination is proved by a new termination criterion for AC rewriting.

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 127R
Location: Ullmann 309
A Calculus for Modular Non-Termination Proofs by Loop Acceleration
PRESENTER: Carsten Fuhs

ABSTRACT. Recently, a calculus to combine various techniques for loop acceleration in a modular way has been introduced [Frohn, TACAS 2020]. We show how to adapt this calculus for proving non-termination. An empirical evaluation demonstrates the applicability of our approach.

Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity
PRESENTER: Jürgen Giesl

ABSTRACT. In previous work we showed that for so-called triangular weakly non-linear loops over rings S like Z, Q, or R, the question of termination can be reduced to the existential fragment of the first-order theory of S. For loops over R, our reduction implies decidability of termination. For loops over Z and Q, it proves semi-decidability of non-termination. In this paper, we show that there is an important class of linear loops where our decision procedure results in an efficient procedure for termination analysis, i.e., where the parameterized complexity of deciding termination is polynomial.

Improved Automatic Complexity Analysis of Integer Programs
PRESENTER: Nils Lommen

ABSTRACT. In former work, we developed an approach for automatic complexity analysis of integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts. In this paper, we show how recent techniques to improve automated termination analysis of integer programs (like the generation of multiphase-linear ranking functions and control-flow refinement) can be integrated into our approach for the inference of runtime bounds. Our approach is implemented in the complexity analysis tool KoAT.

15:30-16:00Coffee Break
16:00-17:00 Session 131N

Business Meeting (WST 2022)

Location: Ullmann 309
18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event