一句话：为抽象解释的数据流分析建立概率化置信度理论框架，量化分析结果的局部完备性精度。
抽象解释是静态程序分析的基础框架，它以过近似保证可靠性（无漏报），但因不完备而常产生误报。已有工作尝试用概率技术为告警计算置信度，但大多依赖经验直觉、缺乏理论基础。本文将数据流分析的置信度问题严格定义为：在与该抽象解释一致的程序的分布下，计算抽象解释器对被采样程序局部完备（locally complete）的概率。为此，作者提出组合式指称语义 ⟨⟨·⟩⟩，据此推导程序输出的分布，从而计算这些置信概率；为保证计算的可处理性，又提出一个下近似语义 ⟨⟨·⟩⟩_lc。论文证明了这两种语义的正确性，从而为用概率量化静态程序分析的精度奠定了理论基础。
Abstract interpretation has served as a foundational framework for static program analysis, enabling the over approximation of program semantics to be sound (i.e., no false negatives) but often at the cost of false alarms due to incompleteness. Although prior efforts to address false alarms have incorporated probabilistic techniques to compute confidence values for alarms, these methods are largely guided by empirical intuitions and lack a theoretical foundation. This paper bridges this gap by proposing a principled framework to quantify the confidence in results produced by a dataflow analysis based on abstract interpretation. Specifically, we define the problem as calculating the probability of the abstract interpreter being locally complete for a sampled program from the distribution of programs consistent with such abstract interpretation. By proposing a compositional denotational semantics ⟨⟨· ⟩⟩, we derive the distribution of program outputs to compute those confidence probabilities. Moreover, to ensure tractability, we propose another denotational semantics ⟨⟨· ⟩⟩ lc that under-approximates ⟨⟨· ⟩⟩. The paper proves both the correctness of the two semantics, and therefore establishes a theoretical foundation for quantifying the precision of static program analysis with probabilities.
@article{ShiJZ26,
title = {Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities},
author = {Yuanfeng Shi and Ziyue Jin and Xin Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808351}
}