Lifting On-Demand Analysis to Higher-Order Languages
summary
Claims an on-demand algorithm that bootstraps call graph construction by interleaving two on-demand data‑flow queries, formalizes the method as an abstract-domain combinator and proved sound in Isabelle/HOL. Prototype for a JavaScript subset uses Synchronized Push-Down Systems and QuickCheck-generated tests; evaluation shows resolving a few call sites issues far fewer additional queries than whole-program analysis, and parallelism reduces wall-clock time though CPU time can rise. Artifact and Isabelle theories are available online.
AI-written summary · about
chapters (9)
- 0:00On-demand callgraph construction
- 2:29Demand-driven callgraph analysis
- 8:44Handling cycles in queries
- 11:52Soundness for callgraph parts
- 14:41Soundness assumptions for points-to
- 17:06Implementation and evaluation
- 20:37Contributions and future work
- 20:59Q&A: Whole-program tools
- 22:02Q&A: Speculative execution & ML