paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Quantitative Symbolic Non-Equivalence Analysis

定量符号非等价分析
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 4/10 · 该论文属于程序分析与抽象解释领域，研究定量符号非等价分析，但未涉及LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心关注点，与用户画像中的PL与AI交叉方向匹配度有限。引用 1 inbox
Laboni Sarker, Tevfik Bultan
程序分析与抽象解释
crossref: 2026-09-12

AI 速览

一句话：提出定量符号非等价分析，可量化程序行为差异并展示其在 EqBench 上对 C 程序版本非等价推理的有效性。

现有等价性分析主要判断不同程序或同一程序的不同版本是否具有完全相同的行为，但针对“非等价”的细致、定量推理技术仍然缺乏。本文提出定量符号非等价分析（quantitative symbolic non-equivalence analysis），以符号化方式对程序间行为差异进行量化刻画，而不仅给出等价/非等价的二元结论。作者在 EqBench——目前最大的等价性分析基准——上评估该方法，并展示其可用于推理不同版本 C 程序的非等价性。实验覆盖该基准并验证了其有效性。

问题
已有大量等价性分析研究，但缺少对程序非等价性进行细致、定量推理的技术。
方法
提出定量符号非等价分析，以符号化方式量化程序间行为差异，而不仅是给出等价/非等价的二元判断。
评估
在目前最大的等价性分析基准 EqBench 上评估有效性，并展示其用于推理不同版本 C 程序非等价性的能力。
原文摘要（Abstract）

Equivalence analysis focuses on assessing whether different programs, or different versions of a program, exhibit identical behavior. While extensive research has been done on equivalence analysis, there is a lack of detailed and quantitative reasoning techniques for non-equivalence. In this paper we introduce quantitative symbolic non-equivalence analysis and evaluate its effectiveness on the EqBench [3] benchmark (the largest available benchmark for equivalence analysis), and demonstrate how it can be used for reasoning about the non-equivalence of different versions of C programs.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot8368,
  title = {Quantitative Symbolic Non-Equivalence Analysis},
  author = {Laboni Sarker and Tevfik Bultan},
  booktitle = {ASE},
  year = {2024},
  doi = {10.1145/3691620.3695324}
}