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 NovDisplayed time zone: (UTC) Coordinated Universal Time change
01:00 - 01:30 | |||
01:00 2mTalk | ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code Research Papers Sahar Badihi University of British Columbia, Canada, Faridah Akinotcho University of British Columbia, Canada, Yi Li Nanyang Technological University, Julia Rubin University of British Columbia, Canada DOI Pre-print | ||
01:03 1mTalk | Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java Research Papers Vaibhav Sharma University of Minnesota, USA, Soha Hussein University of Minnesota, USA / Ain Shams University, Egypt, Michael Whalen University of Minnesota, USA, Stephen McCamant University of Minnesota, USA, Willem Visser Stellenbosch University, South Africa DOI | ||
01:05 1mTalk | PCA: Memory Leak Detection using Partial Call-Path Analysis Tool Demos Wen Li , Haipeng Cai Washington State University, USA, Yulei Sui University of Technology Sydney, David Manz Pacific Northwest National Laboratory, USA DOI | ||
01:07 1mTalk | SWAN: A Static Analysis Framework for Swift Tool Demos Daniil Tiganov University of Alberta, Canada, Jeff Cho University of Alberta, Karim Ali University of Alberta, Julian Dolby IBM Research, USA DOI | ||
01:09 1mTalk | UBITect: A Precise and Scalable Method to Detect Use-before-Initialization Bugs in Linux Kernel Research Papers Yizhuo Zhai University of California at Riverside, USA, Yu Hao University of California at Riverside, USA, Hang Zhang University of California at Riverside, USA, Daimeng Wang University of California at Riverside, USA, Chengyu Song University of California at Riverside, USA, Zhiyun Qian University of California at Riverside, USA, Mohsen Lesani University of California at Riverside, USA, Srikanth V. Krishnamurthy University of California at Riverside, USA, Paul Yu U.S. Army Research Laboratory, USA DOI | ||
01:11 19mTalk | Conversations on Static Analysis Paper Presentations Daniil Tiganov University of Alberta, Canada, Haipeng Cai Washington State University, USA, Sahar Badihi University of British Columbia, Canada, Yizhuo Zhai University of California at Riverside, USA, M: Paul Gazzillo University of Central Florida | ||