paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Higher-order Demand-driven Program Analysis

高阶需求驱动程序分析
TOPLAS 41(3)2019匹配度 3/10 · 该论文属于纯程序语言与静态分析方向,研究高阶程序的需求驱动分析,与用户核心关注的 LLM/Agent、浮点程序分析、贝叶斯程序分析等交叉方向无直接关联。仅因同属静态分析领域而有边缘相关性。引用 6 inbox
Leandro Facchinetti, Zachary Palmer, Scott Smith
crossref: 2026-09-10

AI 速览

一句话:提出高阶需求驱动程序分析 DDPA,将需求驱动查找扩展到高阶程序,保持流/上下文敏感与多项式复杂度。

针对高阶函数语言难以同时获得精确且高效程序分析的问题,论文提出高阶需求驱动程序分析(DDPA)。该方法将一阶分析中著名的需求驱动查找技术扩展到高阶程序,并针对非局部变量值的按需求值提出新机制。DDPA 具有流敏感和上下文敏感特性,且可证明为多项式时间。为高效实现,作者开发了新的下推自动机元编程框架——Pushdown Reachability 自动机。论文对分析进行了形式化并证明其可靠性,同时描述了实现;摘要未报告具体实验评估结果。

问题
如何为含高阶函数的语言设计既精确又高效的程序分析,尤其是将一阶需求驱动查找推广到高阶场景。
方法
定义 DDPA,引入面向非局部变量值的需求驱动查找方法,使其流敏感、上下文敏感且多项式时间;并开发 Pushdown Reachability 自动机元编程框架来实现。
评估
论文形式化分析并证明其可靠性,并描述了实现;摘要未给出具体实验评估数据。
原文摘要(Abstract)

Developing accurate and efficient program analyses for languages with higher-order functions is known to be difficult. Here we define a new higher-order program analysis, Demand-Driven Program Analysis (DDPA), which extends well-known demand-driven lookup techniques found in first-order program analyses to higher-order programs. This task presents several unique challenges to obtain good accuracy, including the need for a new method for demand-driven lookup of non-local variable values. DDPA is flow- and context-sensitive and provably polynomial-time. To efficiently implement DDPA, we develop a novel pushdown automaton metaprogramming framework, the Pushdown Reachability automaton. The analysis is formalized and proved sound, and an implementation is described.

链接与引用

DOI 原文 ·

BibTeX
@article{paperbot708,
  title = {Higher-order Demand-driven Program Analysis},
  author = {Leandro Facchinetti and Zachary Palmer and Scott Smith},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {41},
  number = {3},
  year = {2019},
  doi = {10.1145/3310340}
}