next day
all days

View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 125Q: Invited talk
Termination Checking and Invariant Synthesis for Affine Programs

ABSTRACT. In this talk we consider foundational questions in proving termination and synthesising invariants for affine programs---program whose assignments are given by affine expressions. We focus in particular on simple linear loops and consider both algebraic and semi-algebraic invariants. We emphasize the close relationship between deciding termination and constructing invariants and highlight mathematical tools in Diophantine approximation and algebraic geometry that underlie recent progress on these problems.

10:30-11:00Coffee Break
11:00-12:30 Session 127Q: Program termination and orderings (I)
Procedure-Modular Termination Analysis

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.

GPO: A Path Ordering for Graphs

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.

Objective and Subjective Specifications

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.

12:30-14:00Lunch Break
14:00-15:30 Session 128Q: Program termination and orderings (II)
Comparing on Strings: Semantic Kachinuki Order
SPEAKER: Alfons Geser

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.

Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions

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.

Well-founded models in proofs of termination

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.

15:30-16:00Coffee Break
16:00-18:00 Session 130P: Termination Competition (report and short talks)

TERMCOMP 2018 - Report

Presentation of tool papers:

  • M. Brockschmidt, S. Dollase, F. Emrich, F. Frohn, C. Fuhs, J. Giesl, M. Hark, J. Hensel, D. Korzeniewski, M. Naaf, T. Ströder. AProVE at the Termination Competition 2018
  • Florian Messner and Christian Sternagel. TermComp 2018 Participant: TTT2
  • Dieter Hofbauer. MultumNonMulta at TermComp 2018
  • Raúl Gutiérrez and Salvador Lucas. MU-TERM at the 2018 Termination Competition
  • Jesús J. Doménech and Samir Genaim. iRankFinder
19:15-21:30 Workshops dinner at Magdalen College

Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).