Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions
Authors:
- 1 January 1999
- book chapter
- Published by Springer Nature
- p. 470-482
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Deciding Equality Formulas by Small Domains Instantiations1999
- Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking1998
- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification1998
- BDD based procedures for a theory of equality with uninterpreted functions1998
- Herbrand automata for hardware verification1998
- Automatic verification of pipelined microprocessor control1994
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980