Size-Change Termination as a Contract
Program termination is an undecidable, yet important, property relevant to program verification, optimization, debugging, partial evaluation, and dependently-typed programming, among many other topics. This has given rise to a large body of work on static methods for conservatively predicting or enforcing termination. A simple effective approach is the size-change termination (SCT) method, which operates in two-phases: (1) abstract programs into "size-change graphs," and (2) check these graphs for the size-change property: the existence of paths that lead to infinitely decreasing value sequences. This paper explores the termination problem starting from a different vantage point: we propose transposing the two phases of the SCT analysis by developing an operational semantics that accounts for the run time checking of the size-change property, postponing program abstraction or avoiding it entirely. This choice has two important consequences: SCT can be monitored and enforced at run-time and termination analysis can be rephrased as a traditional safety property and computed using existing abstract interpretation methods. We formulate this run-time size-change check as a contract. This contributes the first run-time mechanism for checking termination in a general-purporse programming language. The result nicely compliments existing contracts that enforce partial correctness to obtain the first contracts for total correctness. Our approach combines the robustness of SCT with precise information available at run-time. To obtain a sound and computable analysis, it is possible to apply existing abstract interpretation techniques directly to the operational semantics; there is no need for an abstraction tailored to size-change graphs. We apply higher-order symbolic execution to obtain a novel termination analysis that is competitive with existing, purpose-built termination analyzers.
NurtureToken New!

Token crowdsale for this paper ends in

Buy Nurture Tokens

Authors

Are you an author of this paper? Check the Twitter handle we have for you is correct.

Phuc C. Nguyen (add twitter)
Thomas Gilray (edit)
Sam Tobin-Hochstadt (edit)
David Van Horn (edit)
Ask The Authors

Ask the authors of this paper a question or leave a comment.

Read it. Rate it.
#1. Which part of the paper did you read?

#2. The paper contains new data or analyses that is openly accessible?
#3. The conclusion is supported by the data and analyses?
#4. The conclusion is of scientific interest?
#5. The result is likely to lead to future research?

Github
User:
None (add)
Repo:
None (add)
Stargazers:
0
Forks:
0
Open Issues:
0
Network:
0
Subscribers:
0
Language:
None
Youtube
Link:
None (add)
Views:
0
Likes:
0
Dislikes:
0
Favorites:
0
Comments:
0
Other
Sample Sizes (N=):
Inserted:
Words Total:
Words Unique:
Source:
Abstract:
None
08/07/18 05:54PM
10,296
3,018
Tweets
lambda_calculus: More bad news: Size-Change Termination as a Contract w/ @pnguyen0112 @tomgilray & @samth WILL be appearing at @PLDI. But don't worry, it's available open-access on @arxiv! (We also paid to make it open-access on the DL.) https://t.co/8dlL8wOGR7
JKPappas: RT @lambda_calculus: New work by @pnguyen0112 @tomgilray @samth and me: Size-Change Termination as a Contract https://t.co/8dlL8wOGR7
krismicinski: RT @lambda_calculus: New work by @pnguyen0112 @tomgilray @samth and me: Size-Change Termination as a Contract https://t.co/8dlL8wOGR7
tomgilray: RT @lambda_calculus: New work by @pnguyen0112 @tomgilray @samth and me: Size-Change Termination as a Contract https://t.co/8dlL8wOGR7
umiacs: RT @lambda_calculus: New work by @pnguyen0112 @tomgilray @samth and me: Size-Change Termination as a Contract https://t.co/8dlL8wOGR7
lambda_calculus: New work by @pnguyen0112 @tomgilray @samth and me: Size-Change Termination as a Contract https://t.co/8dlL8wOGR7
Images
Related