BDD based procedures for a theory of equality with uninterpreted functions

Anuj Goel*, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

7 Scopus citations


The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for such verification paradigms to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the variables. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach.

Original languageEnglish (US)
Pages (from-to)205-224
Number of pages20
JournalFormal Methods in System Design
Issue number3
StatePublished - May 1 2003


  • BDDs
  • Logic of equality
  • Uninterpreted functions

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'BDD based procedures for a theory of equality with uninterpreted functions'. Together they form a unique fingerprint.

Cite this