Scaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural(…)
summary
Applies graph neural networks to Datalog-derived graphs to prune abstraction parameters, then solves the reduced max‑sat refinement problem with a solver; transforms Datalog hyperedges into bidirectional edges on Datalog hypergraphs so one GNN model generalizes across analyses without feature engineering. Evaluated on pointer and typestate analyses: answers 2.83× and 1.5× more queries, prunes 88–95% of parameters, trains on small benchmarks and generalizes to large ones, and shows GNN alone over‑ or under‑refines while the GNN‑pruned max‑sat combo succeeds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:26Obstruction refinement challenges
- 3:36Datalog and graph neural networks
- 5:46Pointer analysis example
- 8:17Pointer analysis in Datalog
- 10:05Hypergraph transformations
- 11:50Training neural refinements
- 13:17Experimental results
- 16:50Conclusion
- 17:12Q&A
related talks
16mPreview: Graph NNs
01h 01mToward Universal Graph Representations: Foundations and Frontiers of Graph Foundation Models
39mUsing Graph Neural Networks to Embrace the Dependency Within Your Data
15mOn Abstraction Refinement for Bayesian Program Analysis
27mProof Minimization in Neural Network Verification
11mLearning Semantic Program Embeddings with Graph Interval Neural Network
15mGauss: Program Synthesis by Reasoning Over Graphs
15mIdentifying and Analyzing Pitfalls in GNN Systems