Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities

Abstract

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 ⟨ ⟨ ⋅ ⟩ ⟩ l c 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.