ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code
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.
Fri 13 Nov Times are displayed in time zone: (UTC) Coordinated Universal Time change
| 01:00 - 01:02 Talk | ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code Research Papers Sahar BadihiUniversity of British Columbia, Canada, Faridah AkinotchoUniversity of British Columbia, Canada, Yi LiNanyang Technological University, Singapore, Julia RubinUniversity of British Columbia, Canada DOI Pre-print | ||
| 01:03 - 01:04 Talk | Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java Research Papers Vaibhav SharmaUniversity of Minnesota, USA, Soha HusseinUniversity of Minnesota, USA / Ain Shams University, Egypt, Michael WhalenUniversity of Minnesota, USA, Stephen McCamantUniversity of Minnesota, USA, Willem VisserStellenbosch University, South Africa DOI | ||
| 01:05 - 01:06 Talk | PCA: Memory Leak Detection using Partial Call-Path Analysis Tool Demos Wen Li, Haipeng CaiWashington State University, USA, Yulei SuiUniversity of Technology Sydney, David ManzPacific Northwest National Laboratory, USA DOI | ||
| 01:07 - 01:08 Talk | SWAN: A Static Analysis Framework for Swift Tool Demos Daniil TiganovUniversity of Alberta, Canada, Jeff ChoUniversity of Alberta, Karim AliUniversity of Alberta, Julian DolbyIBM Research, USA DOI | ||
| 01:09 - 01:10 Talk | UBITect: A Precise and Scalable Method to Detect Use-before-Initialization Bugs in Linux Kernel Research Papers Yizhuo ZhaiUniversity of California at Riverside, USA, Yu HaoUniversity of California at Riverside, USA, Hang ZhangUniversity of California at Riverside, USA, Daimeng WangUniversity of California at Riverside, USA, Chengyu SongUniversity of California at Riverside, USA, Zhiyun QianUniversity of California at Riverside, USA, Mohsen LesaniUniversity of California at Riverside, USA, Srikanth V. KrishnamurthyUniversity of California at Riverside, USA, Paul YuU.S. Army Research Laboratory, USA DOI | ||
| 01:11 - 01:30 Talk | Conversations on Static Analysis Paper Presentations Daniil TiganovUniversity of Alberta, Canada, Haipeng CaiWashington State University, USA, Sahar BadihiUniversity of British Columbia, Canada, Yizhuo ZhaiUniversity of California at Riverside, USA, M: Paul GazzilloUniversity of Central Florida | ||