Interesting Findings!

My equivalence analysis tool, built on angr for symbolic analysis of program binaries, enables precise detection of subtle behavioral differences. In the EqBench benchmark, it identified three cases where integer overflow causes two programs—originally marked as "equivalent"—to behave differently. The figure illustrates one such case: the benchmark assumes that multiplying three positive or three negative values always yields a result with the same sign. However, due to 32-bit integer overflow in C, even multiplying three positive values (e.g., x = 1291) can yield a negative result, breaking the assumed equivalence. This finding highlights both the need for binary-level analysis and the effectiveness of my tool in uncovering such hidden issues.