[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Byron Cook & Andreas Podelski & Andrey Rybalchenko
- Proving program termination
- Commun ACM V54n5(May 2011)pp88-98
[ 1941487.1941509 ]
- =DEMO MATHEMATICS TERMINATION LOGIC DISJUNCTIVE
- Instead of proving that the transition relation R is a sub-relation of a well-founded relation T:
One can try to prove that
- R^(1..*) ==> | [i:1..n] T[i],
where each T[i] is well-founded.
- Claims that "Ramsey's Theorem" implies that only a finite collection of T's need be considered.
- Adding extra statements and assertions to the code can express termination as invariants.
For example, to verify that a variable is decreasing but positive:
assert( oldx > x && x > 0 );
- Tools can then verify the invariants.
- Compare Andreas Blass and Yuri Gurevich. ACM Trans Comp Logic (Dec 2006) pp1-25
[ download?doi=10.1.1.146.4485&rep=rep1&type=pdf ]
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]