Marc Brockschmidt, Byron Cook, and Carsten Fuhs
One of the difficulties of proving program termination is managing the
subtle interplay between the finding of a termination argument and the finding of the argument's supporting invariant.
In this paper we propose a new mechanism that facilitates better cooperation between these two types of reasoning.
In an experimental evaluation we find that our new method leads to dramatic performance improvements.