The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Better termination proving through cooperation
Marc Brockschmidt, Byron Cook, and Carsten Fuhs
AIB 2013-06
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.
