Better termination proving through cooperation

  • Marc Brockschmidt ,
  • Byron Cook ,
  • Carsten Fuhs

CAV proceedings |

Published by Springer

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.