Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks

CEGAR-based abstraction refinement often relies on constraint solving, which can struggle to scale to large Datalog analyses. This work uses graph neural networks to prune unhelpful abstraction parameters from Datalog derivation graphs before MaxSAT-based refinement, yielding smaller constraint problems that speed up constraint solving and more effective refinements that reduce the number of the refinement iterations.

Our approach is general and does not require heavy domain knowledge for different analyses. Experiments on pointer and typestate analyses show that this approach answers 2.83x and 1.5x as many queries, respectively, as the baseline on large programs. It also runs faster on programs where both approaches terminate, and its timeout frequency is about 30% of the baseline’s.