Call-Guarded Abstract Definitional InterpretersDistinguished Paper
Over the last 15 years, several popular systematic abstraction frameworks have emerged—frameworks that allow a static analysis to be derived by systematically transforming a concrete semantics. These frameworks guarantee computability of the resulting artifact by the application of an a priori abstraction which induces a particular finitization in the execution space. While effective, this abstraction occurs without regard for program structure, subjecting each program point to the same fixed degree of context sensitivity. In this paper, we present CGADI, an enhancement to systematic abstraction frameworks based on definitional interpreters which defers abstraction until a parameterized safety property signals that it should be applied. We then examine this enhanced framework instantiated with two such safety properties: a simple reentrancy property which detects non-recursive portions of program execution, and a size change property which detects evaluation paths destined to converge by virtue of appropriately decreasing values along them. The result is that CGADI can operate in the fully-precise concrete space for portions of execution without forfeiting computability. Our evaluation demonstrates that CGADI is able to produce a higher number of precise results than a corresponding CFA at relatively low cost and that, with no special treatment, CGADI can handle many programming patterns targeted by specific analysis techniques.
Mon 13 OctDisplayed time zone: Perth change
13:40 - 15:20 | |||
13:40 25mTalk | Call-Guarded Abstract Definitional InterpretersDistinguished Paper ICFP Papers Kimball Germane Brigham Young University DOI | ||
14:05 25mTalk | Effectful Lenses: There and Back with Different MonadsDistinguished Paper ICFP Papers DOI | ||
14:30 25mTalk | First-Order LazinessDistinguished Paper ICFP Papers Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh DOI Pre-print | ||
14:55 25mTalk | Multi-stage Programming with Splice VariablesDistinguished Paper ICFP Papers DOI | ||
