Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-...
summary
Claims an on-demand APA pipeline that, after n·log n·k preprocessing, answers any pairwise path-summary query in O(k) per query by precomputing only O(n log n) “special” summaries instead of all n^2 pairs. It hinges on real CFGs having low treewidth (and call graphs low treedepth), uses a centroid decomposition of the tree decomposition to bound special queries, and reports experiments on IFDS/BDD-based analyses that beat running fresh APA per query by orders of magnitude.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:20Problem context
- 1:02Control flow graphs
- 3:53On-demand analysis
- 5:18Intraprocedural algorithm
- 7:25Tree decomposition
- 9:11Precomputing queries
- 12:40Centroid decomposition
- 13:21Interprocedural case
- 14:02Experimental results
- 15:06Conclusion
- 15:28Q&A
related talks
15mAutomatic Synthesis of Data-Flow Analyzers
31mInterprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries
20mSimple and Efficient Computation of Minimal Weak Control Closure
40mUtilizing Structure in Combinatorial Solving and Reasoning
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
53mData Deduplication For Redundant Graph Structures Files
52mProgramming Obesity: A Code Health Epidemic
24mEfficient Algorithms for Dynamic Bidirected Dyck-Reachability