Context-Free Language Reachability via Skewed Tabulation
summary
Proposes skewed tabulation that rewrites grammars and treats certain summary edges as propagating edges so the solver avoids generating intermediary summary edges for recursive nonterminals, implemented as an online CFL‑reachability solver and a cheap grammar transform (<1s). Applied to alias, value‑flow, and taint analyses on SPEC2017 and compared to RHS tabulation, it reports 3.34× speedup (alias), 1.13× (value flow), 2.05× (taint) and memory drops of about 60%, 20%, 63% respectively, artifact available on Zenodo.
AI-written summary · about
chapters (16)
- 0:00Skewed tabulation for CFL reachability
- 0:23Context-free language reachability
- 1:08CFL reachability background
- 2:33Tabulation method summary edges
- 4:43Summary degree inefficiencies
- 6:09Motivation for dynamic skewing
- 7:13Static grammar transformation
- 9:02Propagating recursive behavior
- 10:05Dynamic skewing with edges
- 11:51Algorithm modifications
- 12:53Formal guarantees
- 13:34Evaluation benchmarks
- 14:17Reducing non-summary edges
- 15:23Performance improvements
- 17:10Conclusion
- 18:14Q&A
related talks
17mIterative-Epoch Online Cycle Elimination for Context-Free Language Reachability
17mA Better Approximation for Interleaved Dyck Reachability
15mRecursive State Machine Guided Graph Folding for Context-Free Language Reachability
15mFaster Reachability Analysis for LR(1) Parsers
14mFast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
21mFlow-Analysis-Based Closure Optimization
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
24mBounded Treewidth, Multiple Context-Free Grammars, and Downward Closures