Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Better termination proving through cooperation

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.


Publication typeInproceedings
Published inCAV
> Publications > Better termination proving through cooperation