Paper Info
Title
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations
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 (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.
Year
DOI
Venue
2001
10.1007/3-540-44585-4_20
CAV
Keywords
Field
DocType
high-level microprocessors,validity checking,equality validity checker,boolean satisfiability,conservative transformations,automatic formal verification,propositional formula,positive equality,uninterpreted functions,vliw microprocessors,exploiting positive equality,formal verification
Discrete mathematics,Very long instruction word,Computer science,Satisfiability,Boolean satisfiability problem,Correctness,Algorithm,Propositional calculus,Theoretical computer science,Propositional formula,Formal verification,Hardware description language
Conference
Volume
ISSN
ISBN
2102
0302-9743
3-540-42345-1
Citations 
PageRank 
References 
10
0.69
16
Authors
2
Name
Order
Citations
PageRank
Miroslav N. Velev195360.17
Randal E. Bryant292041194.64