Range Allocation for Equivalence Logic

  • Amir Pnueli
  • Yoav Rodeh
  • Ofer Shtrichman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


The range allocation problem was recently introduced as part of an efficient decision procedure for deciding satisfiability of equivalence logic formulas with or without uninterpreted functions. These type of formulas are mainly used when proving equivalence or refinement between systems (hardware designs, compiler’s translation, etc). The problem is to find in polynomial time a small finite domain for each of the variables in an equality formula φ, such that φ is valid if and only if it is valid over this small domain. The heuristic that was presented for finding small domains was static, i.e. it finds a small set of integer constants for each variable. In this paper we show new, more flexible range allocation methods. We also show the limitations of these and other related approaches by proving a lower bound on the size of the state space generated by such procedures. To prove this lower bound we reduce the question to a graph theoretic counting question, which we believe to be of independent interest.


State Space Equivalence Logic Small Domain Boolean Variable Boolean Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. BD94.
    J.R. Burch and D.L. Dill, “Automatic Verification of Microprocessor Control”, In Computer-Aided Verification CAV’ 94.Google Scholar
  2. BDL96.
    Clark W. Barrett, David L. Dill and Jeremy R. Levitt, “Validity Checking for Combinations of Theories with Equality”, In Formal Methods in Computer Aided Design FMCAD’ 96.Google Scholar
  3. BV00.
    R. E. Bryant and M. N. Velev, “Boolean satisfiability with transitivity constraints”, In Computer-Aided Verification CAV 2000.Google Scholar
  4. GSZAS98.
    A. Goel, K. Sajid, H. Zhou, A. Aziz and V. Singhal, “BDD Based Procedures for a Theory of Equality with Uninterpreted Functions”, In Computer-Aided Verification CAV’ 98.Google Scholar
  5. PRSS98.
    A. Pnueli, Y. Rodeh, M. Seigel and O. Shtrichman, “Deciding Equality Formulas by Small Domain Instantiations”, In Computer-Aided Verification CAV’ 99.Google Scholar
  6. PSS98.
    A. Pnueli, M. Siegel and O. Shtrichman, “Translation Validation for Synchronous Languages”, In International Colloquium on Automata, Languages and Programming ICALP’ 98.Google Scholar
  7. RS01.
    Y. Rodeh and O. Shtrichman, “Finite Instantiations in Equivalence Logic with Uninterpreted Functions”, In Computer-Aided Verification CAV’ 01.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Amir Pnueli
    • 1
  • Yoav Rodeh
    • 1
    • 2
  • Ofer Shtrichman
    • 1
    • 2
  1. 1.Weizmann Institute of ScienceRehovotIsrael
  2. 2.IBM Haifa Research LaboratoryIsrael

Personalised recommendations