[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

CookPodelskiRybalchenko11

  1. Byron Cook & Andreas Podelski & Andrey Rybalchenko
  2. Proving program termination
  3. Commun ACM V54n5(May 2011)pp88-98 [ 1941487.1941509 ]
  4. =DEMO MATHEMATICS TERMINATION LOGIC DISJUNCTIVE
  5. Instead of proving that the transition relation R is a sub-relation of a well-founded relation T:
  6. R==>T, One can try to prove that
  7. R^(1..*) ==> | [i:1..n] T[i], where each T[i] is well-founded.
  8. Claims that "Ramsey's Theorem" implies that only a finite collection of T's need be considered.
  9. 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 );
        oldx:=x;
  10. Tools can then verify the invariants.
  11. 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 uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]