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.