Tue 25 Jun 2019 15:00 - 15:20 at 229AB - Static Analysis Chair(s): Martin C. Rinard

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 checks as contracts in the style of Findler and Felleisen. The result compliments existing contracts that enforce partial correctness specifications to obtain contracts for total correctness. Our approach combines the robustness of the size-change principle for termination with the precise information available at run-time. It has tunable overhead and can check for nontermination without the conservativeness necessary in static checking. To obtain a sound and computable termination analysis, we apply existing abstract interpretation techniques directly to the operational semantics, avoiding the need for custom abstractions for termination. The resulting analyzer is competitive with with existing, purpose-built analyzers.

Conference Day
Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Static AnalysisPLDI Research Papers at 229AB
Chair(s): Martin C. RinardMassachusetts Institute of Technology
14:00
20m
Talk
Abstract Interpretation under Speculative Execution
PLDI Research Papers
Meng WuVirginia Tech, Chao WangUSC
Media Attached
14:20
20m
Talk
A Fast Analytical Model of Fully Associative Caches
PLDI Research Papers
Tobias GysiETH Zurich, Switzerland, Tobias GrosserETH Zurich, Laurin BrandnerETH Zurich, Switzerland, Torsten HoeflerETH Zurich
Media Attached
14:40
20m
Talk
Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees
PLDI Research Papers
Laith SakkaPurdue University, Kirshanthan SundararajahPurdue University, Ryan R. NewtonIndiana University, Milind KulkarniPurdue University
Media Attached
15:00
20m
Talk
Size-Change Termination as a Contract
PLDI Research Papers
Phúc C. NguyễnUniversity of Maryland, Thomas GilrayUniversity of Maryland, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland, USA
Media Attached