Quantitative Symbolic Non-Equivalence Analysis

Equivalence analysis focuses on assessing whether different programs, or different versions of a program, exhibit identical behavior. While extensive research has been done on equivalence analysis, there is a lack of detailed and quantitative reasoning techniques for non-equivalence. In this paper we introduce quantitative symbolic non-equivalence analysis and evaluate its effectiveness on the EqBench [3] benchmark (the largest available benchmark for equivalence analysis), and demonstrate how it can be used for reasoning about the non-equivalence of different versions of C programs.