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 dramatically speeds up validity checking of formulas in the logic of Equality with Uninterpreted Functions and Memories (EUFM). The logic expresses connectness of high-level microprocessors. We present EVC (Equality Validity Checker) -- a tool that exploits positive equality and other optimizations when translating a formula in EUFM to a propositional formula, which can then be evaluated by any Boolean satisfiability (SAT) procedure. EVC has been used for the automatic formal verification of pipelined, superscalar, and VLIW microprocessors.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element