paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Systematic Design of Responsibility Analysis by Abstract Interpretation

基于抽象解释的责任分析的系统化设计
TOPLAS 44(1)2021匹配度 3/10 · 该论文属于抽象解释与程序分析理论,提出责任分析的形式化框架,但未涉及用户核心关注的 LLM/Agent、浮点程序分析或贝叶斯程序分析等交叉方向。虽属静态分析基础工作,但与当前研究画像的直接匹配度有限。引用 5 inbox
Chaoqiang Deng, Patrick Cousot
crossref: 2026-09-10

AI 速览

一句话:提出基于抽象解释的责任分析,用迹语义抽象定义责任,并给出可靠的抽象分析框架。

该文研究程序静态分析中如何自动判定与给定行为对应的责任实体(根因)。作者基于迹语义的抽象提出新的责任定义,并引入观察者认知因素,较现有依赖与因果分析方法在多个示例上更精确。由于具体迹语义一般不可计算,具体责任分析不可判定。为此,文章提出可靠的抽象责任分析框架:通过带迹划分的向前可达性过近似与向后不可能失败可达性的欠/过近似迭代,构造迹划分自动机,并沿其路径确定潜在责任实体的上下界。抽象分析可能损失精度,但保持可靠性,具体责任实体必在抽象结果中被识别。

问题
给定一种关注的行为,如何在程序静态分析中自动确定对应的责任实体(即根因)。
方法
基于迹语义的抽象提出新的责任定义,并设计可靠的抽象责任分析:迭代执行带迹划分的向前可达性过近似以及向后不可能失败可达性的欠/过近似,构造迹划分自动机并沿路径界定潜在责任实体。
评估
在多个示例上,责任分析比现有依赖和因果分析方法更精确;抽象分析虽可能损失精度,但被论证为可靠,具体责任实体必在抽象结果中被找到。
原文摘要(Abstract)

Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples.However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1204,
  title = {The Systematic Design of Responsibility Analysis by Abstract Interpretation},
  author = {Chaoqiang Deng and Patrick Cousot},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {44},
  number = {1},
  year = {2021},
  doi = {10.1145/3484938}
}