ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code
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.
BibTeX
@inproceedings{Badihi-al:FSE20,
author = {Sahar Badihi and
Faridah Akinotcho and
Yi Li and
Julia Rubin},
title = {{ARDiff:} scaling program equivalence checking via iterative abstraction and refinement of common code},
booktitle = {{ESEC/SIGSOFT} {FSE}},
pages = {13--24},
publisher = {{ACM}},
year = {2020},
}