Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions
- 1 January 1999
- book chapter
- Published by Springer Nature
- p. 470-482
- https://doi.org/10.1007/3-540-48683-6_40
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Deciding Equality Formulas by Small Domains InstantiationsPublished by Springer Nature ,1999
- Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence CheckingPublished by Springer Nature ,1998
- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor VerificationPublished by Springer Nature ,1998
- BDD based procedures for a theory of equality with uninterpreted functionsPublished by Springer Nature ,1998
- Herbrand automata for hardware verificationPublished by Springer Nature ,1998
- Automatic verification of pipelined microprocessor controlPublished by Springer Nature ,1994
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980