一句话：提出多重上下文无关语言可达性模型，以可调精度、可判定地近似交错 Dyck 可达性，并给出算法复杂度与实现评估。
上下文无关语言（CFL）可达性是静态分析的标准方法，但表达能力不足以实现高精度；而更强的上下文相关语言形式化又常使可达性问题不可判定。本文引入多重上下文无关语言（MCFL）可达性，作为既具表达力又可处理的静态分析模型。MCFL 由维度 d 和秩 r 参数化形成无限层级，d、r 越大表达力与精度越高。作者构造一族 MCFL 来近似原本不可判定的交错 Dyck 可达性，并给出算法复杂度：r=1 时为 O(n^{2d+1})，r>1 时为 O(n^{dr+1})，同时基于 SETH 与 BMM 假设给出下界，说明 r=1 时算法在 d 各层级上至多差 n 因子、d=1 时最优。最后实现该算法并用于 Android 污点分析：在 11 个基准中 8 个发现全部污染信息，其余 3 个确认过近似所报可达对的 94.3%，首次实现高且可证明的覆盖率。
Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from x to y ?) is phrased as a language reachability problem on a graph G wrt a CFL L . However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis? In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension d and a rank r . Larger d and r yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem. Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed ? We show that the problem takes O n 2 d + 1 time on a graph of n nodes when r = 1 , and O n d r + 1 time when r > 1 . Moreover, we show that when r = 1 , even the simpler membership problem has a lower bound of n 2 d based on the Strong Exponential Time Hypothesis, while reachability for d = 1 has a lower bound of n 3 based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for r = 1 , our algorithm is optimal within a factor n for all levels of the hierarchy based on the dimension d (and fully optimal for d = 1 ). We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. When combined with existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, while it has remarkable coverage (confirming 94.3 % of the reachable pairs reported by the overapproximation) on the remaining 3. To our knowledge, this is the first report of high and provable coverage for this challenging benchmark set.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ConradoKPP25,
title = {Program Analysis via Multiple Context Free Language Reachability},
author = {Giovanna Kobus Conrado and Adam Husted Kjelstrøm and Jaco van de Pol and Andreas Pavlogiannis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704854}
}