{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:15Z","timestamp":1775873595544,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62172017"],"award-info":[{"award-number":["62172017"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Bayesian program analysis is a systematic approach to learn from external information for better accuracy by converting logical deduction in conventional program analysis into Bayesian inference.  \nA key challenge in Bayesian program analysis is how to select program abstractions to effectively generalize from external information.  \nA recent approach addresses this challenge by learning a selection policy on training programs but may result in sub-optimal performance on new programs due to its learning nature and when the training set selection is not ideal.  \nTo address this problem, we propose an approach that is inspired by the framework of counterexample-guided refinement to search for an abstraction on the fly.  \nOur key innovation is to apply the theory of conditional independence to refine the abstraction so that incorrect generalizations can be removed.  \nTo demonstrate the effectiveness of our approach, we have instantiated it on a Bayesian thread-escape analysis and a Bayesian datarace analysis and shown that it significantly improves the performance of the analyses.<\/jats:p>","DOI":"10.1145\/3763166","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3232-3258","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["On Abstraction Refinement for Bayesian Program Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-9656-8889","authenticated-orcid":false,"given":"Yuanfeng","family":"Shi","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2061-0273","authenticated-orcid":false,"given":"Yifan","family":"Zhang","sequence":"additional","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"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1808877.1808883"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_3_1","volume-title":"Formulog: Datalog for SMT-Based Static Analysis (Extended Version). arxiv:2009.08361. arxiv:2009.08361","author":"Bembenek Aaron","year":"2020","unstructured":"Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis (Extended Version). arxiv:2009.08361. arxiv:2009.08361"},{"key":"e_1_2_1_4_1","volume-title":"Pattern recognition and machine learning. 4","author":"Bishop Christopher M","unstructured":"Christopher M Bishop and Nasser M Nasrabadi. 2006. Pattern recognition and machine learning. 4, Springer."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.345"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639949.1640108"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838553"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3087402"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468626"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3436877"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3652136"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.01.003"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555263"},{"key":"e_1_2_1_17_1","volume-title":"An introduction to ROC analysis. Pattern recognition letters, 27, 8","author":"Fawcett Tom","year":"2006","unstructured":"Tom Fawcett. 2006. An introduction to ROC analysis. Pattern recognition letters, 27, 8 (2006), 861\u2013874."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837663"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314616"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462191"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Hyunsu Kim Mukund Raghothaman and Kihong Heo. 2022. Learning Probabilistic Models for Static Analysis Alarms.","DOI":"10.1145\/3510003.3510098"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3088525.3088675"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Ugur Koc Shiyi Wei Jeffrey S Foster Marine Carpuat and Adam A Porter. 2019. An empirical assessment of machine learning approaches for triaging reports of a java static analysis tool. In 2019 12th ieee conference on software testing validation and verification (icst). 288\u2013299.","DOI":"10.1109\/ICST.2019.00036"},{"key":"e_1_2_1_24_1","volume-title":"Probabilistic graphical models: principles and techniques","author":"Koller Daphne","unstructured":"Daphne Koller and Nir Friedman. 2009. Probabilistic graphical models: principles and techniques. MIT press."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00048"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649828"},{"key":"e_1_2_1_27_1","unstructured":"Ziyang Li Saikat Dutta and Mayur Naik. 2024. Llm-assisted static analysis for detecting security vulnerabilities. arXiv preprint arXiv:2405.17238."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786851"},{"key":"e_1_2_1_31_1","volume-title":"Algorithms for Weighted Boolean Optimization. CoRR, abs\/0903.0843","author":"Manquinho Vasco M.","year":"2009","unstructured":"Vasco M. Manquinho, Jo\u00e3o Marques-Silva, and Jordi Planes. 2009. Algorithms for Weighted Boolean Optimization. CoRR, abs\/0903.0843 (2009), arXiv:0903.0843. arxiv:0903.0843"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Ruben Martins Vasco M. Manquinho and In\u00eas Lynce. 2014. Open-WBO: A Modular MaxSAT Solver . In SAT.","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1044834.1044835"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1756006.1859925"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9146-2"},{"key":"e_1_2_1_36_1","volume-title":"Loopy Belief Propagation for Approximate Inference: An Empirical Study. In Conference on Uncertainty in Artificial Intelligence. https:\/\/api.semanticscholar.org\/CorpusID:16462148","author":"Murphy Kevin P.","unstructured":"Kevin P. Murphy, Yair Weiss, and Michael I. Jordan. 1999. Loopy Belief Propagation for Approximate Inference: An Empirical Study. In Conference on Uncertainty in Artificial Intelligence. https:\/\/api.semanticscholar.org\/CorpusID:16462148"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103701"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192417"},{"key":"e_1_2_1_40_1","volume-title":"Applications of Logic Databases","author":"Reps Thomas W","unstructured":"Thomas W Reps. 1995. Demand interprocedural program analysis using logic databases. In Applications of Logic Databases. Springer, 163\u2013196."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_2_1_42_1","unstructured":"Yannis Smaragdakis. 2010. Pick Your Contexts Well : Understanding Object-Sensitivity The Making of a Precise and Scalable Pointer Analysis. https:\/\/api.semanticscholar.org\/CorpusID:9747942"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454026"},{"key":"e_1_2_1_45_1","first-page":"131545","article-title":"LLMDFA: Analyzing Dataflow in Code with Large Language Models","volume":"37","author":"Wang Chengpeng","year":"2024","unstructured":"Chengpeng Wang, Wuqi Zhang, Zian Su, Xiangzhe Xu, Xiaoheng Xie, and Xiangyu Zhang. 2024. LLMDFA: Analyzing Dataflow in Code with Large Language Models. Advances in Neural Information Processing Systems, 37 (2024), 131545\u2013131574.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428205"},{"key":"e_1_2_1_47_1","volume-title":"ACM-SIGPLAN Symposium on Programming Language Design and Implementation. https:\/\/api.semanticscholar.org\/CorpusID:14810646","author":"Whaley John","unstructured":"John Whaley and Monica S. Lam. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In ACM-SIGPLAN Symposium on Programming Language Design and Implementation. https:\/\/api.semanticscholar.org\/CorpusID:14810646"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Xin Zhang Yuanfeng Shi Yifan Zhang. 2025. On Abstraction Refinement for Bayesian Program Analysis (Paper Artifact). https:\/\/doi.org\/10.5281\/zenodo.16917600 10.5281\/zenodo.16917600","DOI":"10.5281\/zenodo.16917600"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133881"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594327"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462185"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3088525.3088563"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649845"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763166","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:44:55Z","timestamp":1760031895000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763166"],"URL":"https:\/\/doi.org\/10.1145\/3763166","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}