Quantitative Symbolic Non-Equivalence Analysis

Abstract

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.

BibTeX

@inproceedings{Sarker-Bultan:ASE24,
  author    = {Laboni Sarker and
               Tevfik Bultan},
  title     = {Quantitative Symbolic {Non-Equivalence} Analysis},
  booktitle = {ASE},
  pages     = {2452--2453},
  publisher = {{ACM}},
  year      = {2024},
}

Quantitative Symbolic Non-Equivalence Analysis

Abstract

Related papers