Sciweavers

CAV
1999
Springer

Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions

14 years 3 months ago
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions
Abstract. In using the logic of equality with unininterpreted functions to verify hardware systems, specific characteristics of the formula describing the correctness condition can be exploited when deciding its validity. We distinguish a class of terms we call “p-terms” for which equality comparisons can appear monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only “maximally diverse” interpretations of the associated function symbols, where every function application yields a different value except when constrained by functional consistency. We present a procedure that translates the original formula into one in propositional logic by interpreting the formula over a domain of fixed-length bit vectors and using vectors of propositi...
Randal E. Bryant, Steven M. German, Miroslav N. Ve
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where CAV
Authors Randal E. Bryant, Steven M. German, Miroslav N. Velev
Comments (0)