EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations

Miroslav N. Velev Randal E. Bryant

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems