
CMUCS03196
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS03196
Revisiting Positive Equality
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
November 2003
CMUCS03196.ps
CMUCS03196.pdf
Keywords: Decision procedures, logic of equality with uninterpreted
functions, verification
This paper provides a stronger result for exploiting positive
equality in the logic of Equality with Uninterpreted Functions (EUF).
Positive equality analysis is used to reduce the number of
interpretations required to check the validity of a formula.
We remove the primary restriction of the previous approach
proposed by Bryant, German and Velev, where positive equality could
be exploited only when all the function applications for a
function symbol appear in positive context. We show that the set
of interpretations considered by our analysis of positive equality
is a subset of the set of interpretations considered by the
previous approach. The paper investigates the obstacles in
exploiting the stronger notion of positive equality (called
robust positive equality) in a decision procedure and provides
a solution for it. We present empirical results on some hardware
and software verification benchmarks.
20 pages
