UnRAVeL Survey Lecture: Jürgen Giesl: Proving Termination with Dependency Pairs

Thursday, May 25, 2023, 12:30pm

Location: Computer Science Center, Building E2, ground floor, B-IT room 5053.2

Speaker: Jürgen Giesl



Until 2000, techniques for automated termination analysis were mainly studied in the areas of logic programming and term rewrite systems (TRSs). However, the power of the available methods and tools was quite limited. In particular, the techniques were not modular and thus, they often failed when applying them to larger programs. Therefore, from 1996 onwards, we started to develop the so-called dependency pair technique to overcome these drawbacks. This technique then evolved into a general framework for modular termination proofs of term rewrite systems and is nowadays used in essentially all termination provers for term rewriting. By applying the dependency pair framework for TRSs as a backend, we also developed techniques for the automated termination analysis of many different programming languages, such as Java, Haskell, or Prolog. While notions like positive almost-sure termination originated in the TRS community, until recently there was hardly any technique available to analyze the termination behavior of probabilistic TRSs (PTRSs). Therefore, in very recent work we started to adapt the dependency pair framework to the probabilistic setting in order to analyze almost-sure termination of PTRSs as well. All these techniques are implemented in our tool AProVE.