ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and... (Video, ESEC/FSE 2020)
"ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code (Video, ESEC/FSE 2020)
Sahar Badihi, Faridah Akinotcho, Yi Li, and Julia Rubin
(University of British Columbia, Canada; University of British Columbia, Canada; Nanyang Technological University, Singapore; University of British Columbia, Canada)
Abstract: 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.
This paper proposes an approach, named ARDiff, for improving the scalability of symbolic-execution-based equivalence checking techniques when comparing syntactically-similar versions of a program, e.g., for verifying the correctness of code upgrades and refactoring. Our approach relies on a set of novel heuristics to determine which parts of the versions’ common code can be effectively pruned during the analysis, reducing the analysis complexity without sacrificing its effectiveness. Furthermore, we devise a new equivalence checking benchmark, extending existing benchmarks with a set of real-life methods containing complex math functions and loops. We evaluate the effectiveness and efficiency of ARDiff on this benchmark and show that it outperforms existing method-level equivalence checking techniques by solving 86% of all equivalent and 55% of non-equivalent cases, compared with 47% to 69% for equivalent and 38% to 52% for non-equivalent cases in related work.
Article: https://doi.org/10.1145/3368089.3409757
Supplementary archive: https://doi.org/10.17605/OSF.IO/CHM2K (Badges: Artifacts Available, Artifacts Evaluated — Functional)
ORCID: https://orcid.org/0000-0003-4562-8208, https://orcid.org/0000-0001-7280-1614
Submitted to the conference by Sahar Badihi on 2020-11-10
Video Tags: Equivalence checking, program analysis, symbolic execution, software evolution, fse20main-p674-p, DOI: 10.1145/3368089.3409757, DOI: 10.17605/OSF.IO/CHM2K, ORCID: 0000-0003-4562-8208, ORCID: 0000-0001-7280-1614, Artifacts Available, Artifacts Evaluated — Functional
Presentation at the ESEC/FSE 2020 conference, November 8–13, 2020, https://2020.esec-fse.org/
Sponsored by ACM SIGSOFT, https://www.sigsoft.org/
Twitter: / fseconf
Reddit: / esecfse "
ISSTA 2021: Panels Celebrating 30 editions of ISSTA (statements from panel in timeband 1)
ISSTA 2021: Panels Celebrating 30 editions of ISSTA (statements from panel in timeband 3)