This program is tentative and subject to change.
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 $\abrackets{\cdot}$, we derive the distribution of program outputs to compute those confidence probabilities. Moreover, to ensure tractability, we propose another denotational semantics $\abrackets{\cdot}^{lc}$ that under-approximates $\abrackets{\cdot}$. 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.
This program is tentative and subject to change.
Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change
15:50 - 17:30 | |||
15:50 20mTalk | Path-Sensitive Abstract Interpretation for WCET Estimation PLDI Research Papers Shangshang Xiao Shandong University, Mengxia Sun Shandong University, Wei Zhang Shandong University, Naijun Zhan Peking University; Zhongguancun Laboratory, Lei Ju Shandong University DOI | ||
16:10 20mTalk | SAIL: Sound Abstract Interpreters with LLMs PLDI Research Papers Qiuhan Gu University of Illinois Urbana-Champaign, Avaljot Singh University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign DOI | ||
16:30 20mTalk | Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation PLDI Research Papers Shaurya Gomber University of Illinois Urbana-Champaign, Debangshu Banerjee University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign DOI Pre-print | ||
16:50 20mTalk | Abstract Interpretation with Confidence PLDI Research Papers DOI | ||
17:10 20mTalk | Optimism in Equality Saturation PLDI Research Papers Russel Arbore University of California at Berkeley, Alvin Cheung University of California at Berkeley, Max Willsey University of California at Berkeley DOI Pre-print | ||