Mutual Refinements of Context-Free Language Reachability
summary
Proposes a modified CFL-reachability algorithm that traces contributing edges per grammar and iteratively removes noncontributing edges across multiple CFL over-approximations, producing a smaller graph each round. Proves existence and uniqueness of a unique fixpoint and preserves cubic time complexity while using cubic space. Implements on two clients: Android taint analysis (Java) and SPEC2017-derived value-flow (LLVM), obtaining about 50% precision improvement on taint and ~10% on value flow, with practical overhead ≈2.5× time and ≈3× memory.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:11Formal language reachability
- 4:00Traditional CFL limits
- 5:45Current approaches and false positives
- 8:11Mutual refinement concept
- 9:14Formal definition
- 9:56Concrete example
- 12:19Theoretical guarantees
- 13:02Complexity analysis
- 14:06Experimental results
- 15:53Future work
- 16:56Generalization Beyond Context-Free Languages
- 17:38Summary
- 17:59Q&A
related talks
16mCounterexample-Guided Correlation Algorithm for Translation Validation
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
16mTermination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
24mWhen to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly
18mA Cocktail Approach to Practical Call Graph Construction
20mSimple and Efficient Computation of Minimal Weak Control Closure
41mDesigning software with complex configurations
58mA New Perspective on Commutativity in Verification