Abstract
We introduce a decision procedure for satisfiability of equivalence logic formulas with uninterpreted functions and predicates. In a previous work ([PRSS99]) we presented a decision procedure for this problem which started by reducing the formula into a formula in equality logic. As a second step, the formula structure was analyzed in order to derive a small range of values for each variable that is sufficient for preserving the formula's satisfiability. Then, a standard BDD based tool was used in order to check the formula under the new small domain. In this paper we change the reduction method and perform a more careful analysis of the formula, which results in significantly smaller domains. Both theoretical and experimental results show that the new method is superior to the previous one and to the method suggested in [BGV99].
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
W. Ackermann, “Solvable Cases of the Decision Problem”, Studies in logic and the foundations of mathematics, North-Holland, Amsterdam, 1954.
J.R. Burch and D.L. Dill, “Automatic Verification of Microprocessor Control”, In Computer-Aided Verification CAV’ 94.
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.
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.
R. Hojati, A. Isles, D. Kirkpatrick and R. K. Brayton, “Verification Using Finite Instantiations and Uninterpreted Functions”, In Formal Methods in Computer Aided Design FMCAD’ 96.
A. Pnueli, Y. Rodeh, M. Siegel and O. Shtrichman, “Deciding Equality Formulas by Small Domain Instantiations”, In Computer-Aided Verification CAV’ 99.
A. Pnueli, M. Siegel and O. Shtrichman, “Translation Validation for Synchronous Languages”, In International Colloquium on Automata, Languages and Programming ICALP’ 98.
A. Pnueli, Y. Rodeh and O. Shtrichman, “Finite Instantiations in Equivalence Logic with Uninterpreted Functions”, Technical report, Weizmann Institute of Science, 2001. http://www.wisdom.weizmann.ac.il/~verify/publication/2001/yrodeh_tr2001.ps.gz
R.E. Bryant and M. Velev, “Bit-level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking”, In Formal Methods in Computer Aided Design FMCAD’ 98.
R.E. Bryant, S. German and M.N. Velev, “Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions”, In Computer-Aided Verification CAV’ 99.
R.E. Bryant and M. N. Velev, “Boolean satisfiability with transitivity constraints”, In Computer-Aided Verification CAV 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rodeh, Y., Shtrichman, O. (2001). Finite Instantiations in Equivalence Logic with Uninterpreted Functions. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_13
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive