{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:12:04Z","timestamp":1784200324373,"version":"3.55.0"},"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. A key challenge in Bayesian program analysis is how to select program abstractions to effectively generalize from external information. A 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. To 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. Our key innovation is to apply the theory of conditional independence to refine the abstraction so that incorrect generalizations can be removed. To 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":3,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2061-0273","authenticated-orcid":false,"given":"Yifan","family":"Zhang","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1515-7145","authenticated-orcid":false,"given":"Xin","family":"Zhang","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","unstructured":"Husain Aljazzar Matthias Kuntz Florian Leitner-Fischer and Stefan Leue. 2010. Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation. In Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems. 25\u201332.","DOI":"10.1145\/1808877.1808883"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_1_4_2","doi-asserted-by":"crossref","unstructured":"Aaron Bembenek Michael Greenberg and Stephen Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis (Extended Version). arXiv:2009.08361 [cs.PL] https:\/\/arxiv.org\/abs\/2009.08361","DOI":"10.1145\/3428209"},{"key":"e_1_3_1_5_2","volume-title":"Pattern recognition and machine learning","author":"Bishop Christopher M","year":"2006","unstructured":"Christopher M Bishop and Nasser M Nasrabadi. 2006. Pattern recognition and machine learning. Vol. 4. Springer."},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Stephen M Blackburn Robin Garner Chris Hoffmann Asjad M Khang Kathryn S McKinley Rotem Bentzur Amer Diwan Daniel Feinberg Daniel Frampton Samuel Z Guyer et al. 2006. The DaCapo benchmarks: Java benchmarking development and analysis. In Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems languages and applications. 169\u2013190.","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.345"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1639949.1640108"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838553"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3087402"},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Tianyi Chen Kihong Heo and Mukund Raghothaman. 2021. Boosting static analysis accuracy with instrumented test executions. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1154\u20131165.","DOI":"10.1145\/3468264.3468626"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3436877"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","unstructured":"Zhaoyang Chu Yao Wan Qian Li Yang Wu Hongyu Zhang Yulei Sui Guandong Xu and Hai Jin. 2024. Graph neural networks for vulnerability detection: A counterfactual explanation. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. 389\u2013401.","DOI":"10.1145\/3650212.3652136"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.01.003"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555263"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.patrec.2005.10.010"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837663"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Kihong Heo Mukund Raghothaman Xujie Si and Mayur Naik. 2019. Continuously reasoning about programs using differential bayesian inference. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 561\u2013575.","DOI":"10.1145\/3314221.3314616"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"George Kastrinis and Yannis Smaragdakis. 2013. Hybrid context-sensitivity for points-to analysis. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (2013). https:\/\/api.semanticscholar.org\/CorpusID:14109210","DOI":"10.1145\/2491956.2462191"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","unstructured":"Hyunsu Kim Mukund Raghothaman and Kihong Heo. 2022. Learning Probabilistic Models for Static Analysis Alarms. (2022).","DOI":"10.1145\/3510003.3510098"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","unstructured":"Ugur Koc Parsa Saadatpanah Jeffrey S Foster and Adam A Porter. 2017. Learning a classifier for false positive error reports emitted by static code analysis tools. In Proceedings of the 1st ACM SIGPLAN international workshop on machine learning and programming languages. 35\u201342.","DOI":"10.1145\/3088525.3088675"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00036"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/1795555"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00048"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649828"},{"key":"e_1_3_1_28_2","unstructured":"Ziyang Li Saikat Dutta and Mayur Naik. 2024. Llm-assisted static analysis for detecting security vulnerabilities. arXiv preprint arXiv:2405.17238 (2024)."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Ravi Mangal Xin Zhang Aditya V Nori and Mayur Naik. 2015. A user-guided approach to program analysis. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. 462\u2013473.","DOI":"10.1145\/2786805.2786851"},{"key":"e_1_3_1_32_2","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 http:\/\/arxiv.org\/abs\/0903.0843"},{"key":"e_1_3_1_33_2","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_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1044834.1044835"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/1756006.1859925"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9146-2"},{"key":"e_1_3_1_37_2","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_3_1_38_2","doi-asserted-by":"crossref","unstructured":"Mayur Naik Alex Aiken and John Whaley. 2006. Effective static race detection for Java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation. 308\u2013319.","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_1_39_2","doi-asserted-by":"crossref","unstructured":"Mayur Naik Hongseok Yang Ghila Castelnuovo and Mooly Sagiv. 2012. Abstractions from tests. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 373\u2013386.","DOI":"10.1145\/2103656.2103701"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Mukund Raghothaman Sulekha Kulkarni Kihong Heo and Mayur Naik. 2018. User-guided program reasoning using Bayesian inference. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 722\u2013735.","DOI":"10.1145\/3192366.3192417"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2207-2_8"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_1_43_2","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_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","unstructured":"Tam\u00e1s Szab\u00f3 Sebastian Erdweg and G\u00e1bor Bergmann. 2021. Incremental whole-program analysis in Datalog with lattices. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1\u201315.","DOI":"10.1145\/3453483.3454026"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.52202\/079017-4181"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428205"},{"key":"e_1_3_1_48_2","doi-asserted-by":"crossref","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","DOI":"10.1145\/996841.996859"},{"key":"e_1_3_1_49_2","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_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133881"},{"key":"e_1_3_1_51_2","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. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 239\u2013248.","DOI":"10.1145\/2594291.2594327"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462185"},{"key":"e_1_3_1_53_2","doi-asserted-by":"crossref","unstructured":"Xin Zhang Xujie Si and Mayur Naik. 2017. Combining the Logical and the Probabilistic in Program Analysis. In Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. 27\u201334.","DOI":"10.1145\/3088525.3088563"},{"key":"e_1_3_1_54_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:17:10Z","timestamp":1784197030000},"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"}}]}}