Size-Change Termination as a Contract
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

TL;DR
This paper introduces a novel approach to program termination analysis by integrating size-change termination checks into runtime contracts, enabling dynamic, precise, and tunable termination verification without static abstraction.
Contribution
It reformulates size-change termination as runtime contracts, allowing dynamic enforcement and analysis, and avoids custom static abstractions by applying existing abstract interpretation techniques.
Findings
Runtime size-change checks enable dynamic termination verification.
The approach is competitive with existing static analyzers.
It allows nontermination detection with tunable overhead.
Abstract
Termination is an important but undecidable program property, which has led to a large body of work on static methods for conservatively predicting or enforcing termination. One such method is the size-change termination approach of Lee, Jones, and Ben-Amram, 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 infinite decreasing sequences. We transpose these two phases with an operational semantics that accounts for the run-time enforcement of the size-change property, postponing (or entirely avoiding) program abstraction. This choice has two key consequences: (1) size-change termination can be checked at run-time and (2) termination can be rephrased as a safety property analyzed using existing methods for systematic abstraction. We formulate run-time size-change…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Software Testing and Debugging Techniques · Formal Methods in Verification
