  Dependency pairs are one of the most powerful techniques to analyze
termination of term rewrite systems (TRSs) automatically. We adapt the
dependency pair framework to the probabilistic setting in order to prove
almost-sure innermost termination of probabilistic TRSs. To evaluate its power,
we implemented the new framework in our tool AProVE.
