Proving program termination in higher order logic
Sava Krstić · 2018
We suggest two simple additions to packages that use wellfounded recursion to justify termination of recursive programs: - The contraction condition, to be proved in cases when termination conditions are di#cult or impossible to extract automatically; - user-supplied inductive invariants in cases of nested recursion.