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.
Zeige Antworten nach Diskussionsstrang
tr-announce@lists.rwth-aachen.de