一句话：提出 ARDiff，通过迭代抽象与精化程序版本间的公共代码，提升程序等价性检查的可扩展性。
程序等价性检查用于判定两个程序版本是否具有相同行为，但主流形式化方法多依赖符号执行，而符号执行在面对循环和非线性算术等复杂语言构造时难以扩展到实际程序。为此，本文提出 ARDiff，其核心思想是识别两个版本中的公共代码，并对这些公共代码进行迭代抽象与精化，从而缩减等价性检查中需要精确推理的代码范围，降低符号执行负担。摘要主要描述了问题与方法，未给出具体实验评估或结果。
Equivalence checking techniques help establish whether two versions of a program exhibit the same behavior. The majority of popular techniques for formally proving/refuting equivalence relies on symbolic execution – a static analysis approach that reasons about program behaviors in terms of symbolic input variables. Yet, symbolic execution is difficult to scale in practice due to complex programming constructs, such as loops and non-linear arithmetic.
DOI 原文 ·
@inproceedings{paperbot5764,
title = {ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code},
author = {Sahar Badihi and Faridah Akinotcho and Yi Li and Julia Rubin},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409757}
}