Better termination proving through cooperation

Marc Brockschmidt, Byron Cook, and Carsten Fuhs

Abstract

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.

Details

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