{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:28:58Z","timestamp":1755217738302,"version":"3.43.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1023\/a:1022988809947","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"205-224","source":"Crossref","is-referenced-by-count":8,"title":["BDD Based Procedures for a Theory of Equality with Uninterpreted Functions"],"prefix":"10.1007","volume":"22","author":[{"given":"Anuj","family":"Goel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khurram","family":"Sajid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hai","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5119202_CR1","unstructured":"W. Ackermann, Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954."},{"key":"5119202_CR2","unstructured":"VSI Alliance. Virtual Socket Interface Proposal 1.0. http:\/\/www.vsi.org\/, September 1996."},{"key":"5119202_CR3","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and J. Levitt, \u201cValidity checking for combinations of theories with equality,\u201d in Formal Methods in CAD, November 1996.","DOI":"10.1007\/BFb0031808"},{"key":"5119202_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, pp. 677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5119202_CR5","doi-asserted-by":"crossref","unstructured":"R. Bryant and Y.A. Chen, \u201cVerification of arithmetic circuits with binary moment diagrams,\u201d in Design Automation Conference, pp. 535\u2013541, June 1995.","DOI":"10.1145\/217474.217583"},{"key":"5119202_CR6","doi-asserted-by":"crossref","unstructured":"R. Bryant and M. Velev, \u201cBoolean satisfiability with transitivity constraints,\u201d in Computer Aided Verification, July 2000.","DOI":"10.21236\/ADA382689"},{"key":"5119202_CR7","doi-asserted-by":"crossref","unstructured":"R.K. Brayton et al., \u201cVIS: A system for verification and synthesis,\u201d in Computer Aided Verification, July 1996.","DOI":"10.1007\/3-540-61474-5_95"},{"key":"5119202_CR8","doi-asserted-by":"crossref","unstructured":"J. Burch and D. Dill, \u201cAutomatic verification of microprocessor control,\u201d in Computer Aided Verification, July 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"5119202_CR9","doi-asserted-by":"crossref","unstructured":"W. Chan, R. Anderson, P. Deame, and D. Notkin, \u201cCombining constraint solving and symbolic model checking for a class of systems with non-linear constraints,\u201d in Computer Aided Verification, July 1997.","DOI":"10.1007\/3-540-63166-6_32"},{"key":"5119202_CR10","unstructured":"T.H. Cormen, C.E. Leiserson, and R.H. Rivest, Introduction to Algorithms, MIT Press, 1989."},{"key":"5119202_CR11","unstructured":"H. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972."},{"key":"5119202_CR12","unstructured":"M.R. Garey and D.S. Johnson, Computers and Intractability, W.H. Freeman and Co., 1979."},{"key":"5119202_CR13","unstructured":"R. Hojati, A. Isles, D. Kirkpatrick, and R. Brayton, \u201cVerification using finite instantiations and uninterpreted functions,\u201d in Formal Methods in CAD, November 1996."},{"key":"5119202_CR14","unstructured":"R. Hojati, A. Kuehlmann, S. German, and R. Brayton, \u201cValidity checking in the theory of equality using finite instantiations,\u201d in Proceedings of the International Workshop on Logic Synthesis, May 1997."},{"key":"5119202_CR15","doi-asserted-by":"crossref","unstructured":"R.B. Jones, D. Dill, and J.R. Burch, \u201cEfficient validity checking for processor validation,\u201d in International Conference on Computer-Aided Design, pp. 2\u20136, 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"5119202_CR16","doi-asserted-by":"crossref","unstructured":"A. Kuehlmann and F. Krohm, \u201cEquivalence checking using cuts and heaps,\u201d in Design Automation Conference, June 1997.","DOI":"10.1145\/266021.266090"},{"key":"5119202_CR17","doi-asserted-by":"crossref","unstructured":"T. Larrabee, \u201cEfficient generation of test patterns using Boolean difference,\u201d in International Test Conference, pp. 795\u2013801, 1989.","DOI":"10.1109\/TEST.1989.82368"},{"key":"5119202_CR18","unstructured":"C.H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994."},{"key":"5119202_CR19","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel, \u201cDeciding equality formulas by small-domains instantiations,\u201d in Computer Aided Verification, July 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"5119202_CR20","unstructured":"R. Rudell, \u201cDynamic variable ordering for binary decision diagrams,\u201d in International Conference on Computer-Aided Design, pp. 42\u201347, November 1993."},{"issue":"2","key":"5119202_CR21","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"R.E. Shostak, \u201cA practical decision procedure for arithmetic with function symbols,\u201d Journal of the ACM, Vol. 26, No. 2, pp. 351\u2013360, 1979.","journal-title":"Journal of the ACM"},{"key":"5119202_CR22","unstructured":"J. Silva and K. Sakallah, \u201cGRASP\u2014A new search algorithm for satisfiability,\u201d in International Conference on Computer-Aided Design, Santa Clara, CA, November 1996."},{"issue":"5","key":"5119202_CR23","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford, \u201cFormal verification of a pipelined microprocessor,\u201d IEEE Software, Vol. 7, No. 5, pp. 52\u201364, September 1990.","journal-title":"IEEE Software"},{"key":"5119202_CR24","doi-asserted-by":"crossref","unstructured":"M. Velev and R. Bryant, \u201cExploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors,\u201d in Design Automation Conference, June 1999.","DOI":"10.1145\/309847.309967"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022988809947.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022988809947\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022988809947.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:12:34Z","timestamp":1754421154000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022988809947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["5119202"],"URL":"https:\/\/doi.org\/10.1023\/a:1022988809947","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}