Proving Program Termination in Higher Order Logic
Proving Program Termination in Higher Order Logic, 2002.
proving program terminationcontraction conditionwellfounded recursionrecursive programhigher order logicMore(6+)
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 difficult or impossible to extract automatically; * user-supplied inductive invariants in cases of nested recursion. We have implemented...More
Full Text (Upload PDF)
PPT (Upload PPT)