A Better Approximation for Interleaved Dyck Reachability
summary
Proposes a concrete overapproximation that extends mutual refinement by adding refined CFLs (grammars that encode parity and endpoint constraints) and an on-demand mutual refinement mode that prunes irrelevant edges for a specific query. Implements incremental grammars and runs experiments on Android taint benchmarks, reducing reported potential false positives from about 55% to ~12% overall and yielding only 51% of reachable pairs on a hard benchmark compared to the prior best alternative.
AI-written summary · about
chapters (11)
- 0:00Interleaved Dyck reachability intro
- 1:28Why interleaved Dyck reachability matters
- 3:15Context-free languages & Dyck paths
- 4:40Limitations of intersection methods
- 6:04Mutual refinement approach
- 7:28Augmenting context-free grammars
- 8:55Adding grammar boundaries
- 9:59On-demand refinement
- 10:40Performance considerations
- 11:43Results & false positives
- 12:25Q&A
related talks
19mContext-Free Language Reachability via Skewed Tabulation
26mOn the Complexity of Bidirected Interleaved Dyck-Reachability
15mFaster Reachability Analysis for LR(1) Parsers
17mIterative-Epoch Online Cycle Elimination for Context-Free Language Reachability
14mFast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
18mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
15mRecursive State Machine Guided Graph Folding for Context-Free Language Reachability
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
