EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations
The property of Positive Equality [2] dramatically speeds up
validity checking of formulas in the logic of Equality with
Uninterpreted Functions and Memories (EUFM) [4]. The logic
expresses correctness of high-level microprocessors. We present
EVC--a tool that exploits Positive Equality and other optimizations
in order to translate a formula in EUFM to a propositional formula,
that can be evaluated with any SAT procedure. EVC has been used
for the automatic formal verification of pipelined, superscalar,
and VLIW microprocessors.
