{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T22:13:38Z","timestamp":1770243218519,"version":"3.49.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>Counterexample-guided abstraction refinement (CEGAR) is a popular approach for automatically selecting abstractions with high precision and low time costs. Existing works cast abstraction refinements as constraintsolving problems. Due to the complexity of these problems, they cannot be scaled to large programs or complex analyses. We propose a novel approach that applies graph neural networks to improve the scalability of CEGAR for Datalog-based program analyses. By constructing graphs directly from the Datalog solver\u2019s calculations, our method then uses a neural network to score abstraction parameters based on the information in these graphs. Then we reform the constraint problems such that the constraint solver ignores parameters with low scores. This in turn reduces the solution space and the size of the constraint problems. Since our graphs are directly constructed from Datalog computation without human effort, our approach can be applied to a broad range of parametric static analyses implemented in Datalog. We evaluate our approach on a pointer analysis and a typestate analysis and our approach can answer 2.83\u00d7 and 1.5\u00d7 as many queries as the baseline approach on large programs for the pointer analysis and the typestate analysis, respectively.<\/jats:p>","DOI":"10.1145\/3689765","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1532-1560","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-6181-6205","authenticated-orcid":false,"given":"Zhenyu","family":"Yan","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1515-7145","authenticated-orcid":false,"given":"Xin","family":"Zhang","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5799-5876","authenticated-orcid":false,"given":"Peng","family":"Di","sequence":"additional","affiliation":[{"name":"Ant Group, Hangzhou, China"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2000 Ashes Suite Collection."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_3_1_5_1","first-page":"243","article-title":"Strictly declarative specification of sophisticated points-to analyses","author":"Bravenboer Martin","year":"2009","unstructured":"Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications. 243-262.","journal-title":"In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133925"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_3_1_8_1","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"Clarke Edmund","year":"2000","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. Springer, 154-169.","journal-title":"Springer"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_20"},{"issue":"2","key":"e_1_3_1_11_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1348250.1348255","article-title":"Effective typestate verification in the presence of aliasing","volume":"17","author":"Stephen J Fink","year":"2008","unstructured":"Stephen J Fink, Eran Yahav, Nurit Dor, G Ramalingam, and Emmanuel Geay. 2008. Effective typestate verification in the presence of aliasing. ACM Transactions on Software Engineering andMethodology (TOSEM) 17, 2 (2008), 1-34.","journal-title":"ACM Transactions on Software Engineering andMethodology (TOSEM)"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-93031-2_18"},{"key":"e_1_3_1_13_1","first-page":"485","article-title":"Abstraction refinement guided by a learnt probabilistic model","author":"Grigore Radu","year":"2016","unstructured":"Radu Grigore and Hongseok Yang. 2016. Abstraction refinement guided by a learnt probabilistic model. In Proceedings of the 43rdAnnual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 485-498.","journal-title":"In Proceedings of the 43rdAnnual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0306-7"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"Mikol\u00e1\u0161 Janota . 2014. MiFuMax\u2014a literate MaxSat solver. 83-88 pages.","DOI":"10.3233\/SAT190103"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293607"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428247"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133924"},{"key":"e_1_3_1_20_1","first-page":"583","volume-title":"Nature","author":"Jumper John","year":"2021","unstructured":"John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ronneberger, Kathryn Tunyasuvunakool, Russ Bates, Augustin Zidek, and Anna Potapenko. 2021. Highly accurate protein structure prediction with AlphaFold. Nature 596, 7873 (2021), 583-589. Publisher: Nature Publishing Group."},{"key":"e_1_3_1_21_1","article-title":"Adam: A method for stochastic optimization","author":"Kingma Diederik P","year":"2014","unstructured":"Diederik P Kingma and Jimmy Ba. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014).","journal-title":"arXiv preprint arXiv:1412.6980"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"e_1_3_1_24_1","unstructured":"Gil Lederman . 2021. Neural Guidance in Constraint Solvers. (2021)."},{"key":"e_1_3_1_25_1","volume-title":"Frontiers in Artificial Intelligence and Applications","author":"Biere Armin","year":"2021","unstructured":"Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). 2021. MaxSAT, Hard and Soft Constraints. Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press. https:\/\/doi.org\/10.3233\/FAIA201007 10.3233\/FAIA201007"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276511"},{"key":"e_1_3_1_27_1","first-page":"129","article-title":"Scalability-first pointer analysis with self-tuning contextsensitivity","author":"Li Yue","year":"2018","unstructured":"Yue Li, Tian Tan, Anders Moller, and Yannis Smaragdakis. 2018b. Scalability-first pointer analysis with self-tuning contextsensitivity. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 129-140.","journal-title":"In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3381915"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591242"},{"key":"e_1_3_1_30_1","first-page":"3","volume-title":"In Proc. icml","author":"Andrew L Maas","year":"2013","unstructured":"Andrew L Maas, Awni Y Hannun, Andrew Y Ng, et al. 2013. Rectifier nonlinearities improve neural network acoustic models. In Proc. icml, Vol. 30. Atlanta, Georgia, USA, 3."},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_19"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_34_1","first-page":"1","article-title":"Parameterized object sensitivity for points-to and side-effect analyses for Java","author":"Milanova Ana","year":"2002","unstructured":"Ana Milanova, Atanas Rountev, and Barbara G Ryder. 2002. Parameterized object sensitivity for points-to and side-effect analyses for Java. In Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis. 1-11.","journal-title":"In Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis"},{"key":"e_1_3_1_35_1","unstructured":"Mayur Naik . 2011. Chord: A versatile platform for program analysis. In Tutorial at ACM Conference on Programming Language Design and Implementation."},{"key":"e_1_3_1_36_1","first-page":"572","volume-title":"In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015","author":"Hakjoo Oh","year":"2015","unstructured":"Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. 2015. Learning a strategy for adapting a program analysis via bayesian optimisation. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 572-588."},{"key":"e_1_3_1_37_1","article-title":"Pytorch: An imperative style, high-performance deep learning library","volume":"32","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. 2019. Pytorch: An imperative style, high-performance deep learning library. Advances in neural information processing systems 32 (2019).","journal-title":"Advances in neural information processing systems"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10844-021-00666-5"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_1_41_1","doi-asserted-by":"crossref","unstructured":"Michael Schlichtkrull Thomas N. Kipf Peter Bloem Rianne Van Den Berg Ivan Titov and Max Welling. 2018. Modeling relational data with graph convolutional networks. Springer 593-607.","DOI":"10.1007\/978-3-319-93417-4_38"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_3_1_43_1","first-page":"693","article-title":"Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code","author":"Shi Qingkai","year":"2018","unstructured":"Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018. Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 693-706.","journal-title":"In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"},{"key":"e_1_3_1_44_1","volume-title":"Control-flow analysis of higher-order languages or taming lambda","author":"Olin Grigsby Shivers","year":"1991","unstructured":"Olin Grigsby Shivers. 1991. Control-flow analysis of higher-order languages or taming lambda. Carnegie Mellon University."},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature16961"},{"key":"e_1_3_1_46_1","first-page":"485","article-title":"Introspective analysis: context-sensitivity, across the board","author":"Smaragdakis Yannis","year":"2014","unstructured":"Yannis Smaragdakis, George Kastrinis, and George Balatsouras. 2014. Introspective analysis: context-sensitivity, across the board. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 485-495.","journal-title":"In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_24"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062360"},{"key":"e_1_3_1_49_1","article-title":"Deep graph library: Towards efficient and scalable deep learning on graphs","author":"Yu Wang Minjie","year":"2019","unstructured":"Minjie Yu Wang . 2019. Deep graph library: Towards efficient and scalable deep learning on graphs. In ICLR workshop on representation learning on graphs and manifolds.","journal-title":"ICLR workshop on representation learning on graphs and manifolds"},{"key":"e_1_3_1_50_1","first-page":"137:1","article-title":"Learning semantic program embeddings with graph interval neural network","volume":"4","author":"Yu Wang","year":"2020","unstructured":"Yu Wang, Ke Wang, Fengjuan Gao, and Linzhang Wang. 2020. Learning semantic program embeddings with graph interval neural network. Proc. ACM Program. Lang. 4, OOPSLA (2020), 137:1-137:27.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_1_51_1","volume-title":"Scaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural Networks (Artifact)","author":"Yan Zhenyu","year":"2024","unstructured":"Zhenyu Yan, Xin Zhang, and Peng Di. 2024. Scaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural Networks (Artifact). https:\/\/doi.org\/10.5281\/zenodo.12663344 10.5281\/zenodo.12663344 Zenodo."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485495"},{"key":"e_1_3_1_54_1","article-title":"NLocalSAT: Boosting local search with solution prediction","author":"Zhang Wenjie","year":"2020","unstructured":"Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang. 2020. NLocalSAT: Boosting local search with solution prediction. arXiv preprint arXiv:2001.09398 (2020).","journal-title":"arXiv preprint arXiv:2001.09398"},{"key":"e_1_3_1_55_1","doi-asserted-by":"crossref","unstructured":"Xin Zhang Ravi Mangal Radu Grigore Mayur Naik and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. 239-248.","DOI":"10.1145\/2594291.2594327"},{"key":"e_1_3_1_56_1","first-page":"707","volume-title":"Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018","author":"He Zhu","year":"2018","unstructured":"He Zhu, Stephen Magill, and Suresh Jagannathan. 2018. A data-driven CHC solver. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 707-721."},{"key":"e_1_3_1_57_1","first-page":"914","article-title":"Chianina: An Evolving Graph System for Flow-and Context-Sensitive Analyses of Million Lines of C Code","author":"Zuo Zhiqiang","year":"2021","unstructured":"Zhiqiang Zuo, Yiyu Zhang, Qiuhong Pan, Shenming Lu, Yue Li, Linzhang Wang, Xuandong Li, and Guoqing Harry Xu. 2021. Chianina: An Evolving Graph System for Flow-and Context-Sensitive Analyses of Million Lines of C Code. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 914-929.","journal-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689765","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689765","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:03:48Z","timestamp":1770195828000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689765"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":56,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689765"],"URL":"https:\/\/doi.org\/10.1145\/3689765","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}