一句话：提出基于条件独立性的抽象精化方法，用反例引导按需搜索抽象，提升贝叶斯程序分析精度。
贝叶斯程序分析将传统程序分析中的逻辑演绎转化为贝叶斯推断，以便利用外部信息提高分析精度。其关键挑战在于如何选择程序抽象，从而有效泛化外部信息。已有方法通过在训练程序上学习选择策略应对，但受学习本质和训练集选择影响，在新程序上可能次优。本文借鉴反例引导精化框架，提出按需搜索抽象的方案。核心创新是应用条件独立理论精化抽象，以去除错误的泛化。作者将方法实例化于贝叶斯线程逃逸分析和贝叶斯数据竞争分析，实验表明其显著提升了分析性能。
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.
@article{paperbot2999,
title = {On Abstraction Refinement for Bayesian Program Analysis},
author = {Yuanfeng Shi and Yifan Zhang and Xin Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763166}
}