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
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Van Gelder, Allen: Producing and verifying extremely large propositional refutations (2012)
- Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
- Toma, Diana; Borrione, Dominique: Formal verification of a SHA-1 circuit core using ACL2 (2005)
- Xu, Ying; Song, Xiaoyu; Cerny, Eduard; Mohamed, Otmane Ait: Model checking for a first-order temporal logic using multiway decision graphs (MDGs) (2004)
- Velev, Miroslav N.: Automatic abstraction of equations in a logic of equality (2003)
- Velev, Miroslav N.; Bryant, Randal E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. (2003)
- Velev, Miroslav N.: Automatic abstraction of memories in the formal verification of superscalar microprocessors (2001)
- Velev, Miroslav N.; Bryant, Randal E.: EVC: A validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality, and conservative transformations (2001)