{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:56:01Z","timestamp":1763726161002},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_40","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T23:22:18Z","timestamp":1191712938000},"page":"470-482","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":40,"title":["Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"German","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miroslav N.","family":"Velev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"40_CR1","unstructured":"W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954."},{"key":"40_CR2","series-title":"Lect Notes Comput Sci","first-page":"187","volume-title":"Formal Methods in Computer-Aided Design FMCAD\u2019 98","author":"S. Berezin","year":"1998","unstructured":"S. Berezin, A. Biere, E. M. Clarke, and Y. Zhu, \u201cCombining symbolic model checking with uninterpreted functions for out of order processor verification,\u201d Formal Methods in Computer-Aided Design FMCAD\u2019 98, G. Gopalakrishnan and P. Windley, eds., LNCS 1522, Springer-Verlag, November, 1998, pp. 187\u2013201."},{"key":"40_CR3","unstructured":"R. E. Bryant, S. German, and M. N. Velev, \u201cProcessor verification using efficient reductions of the logic of uninterpreted functions to propositional logic,\u201d Technical report CMU-CS-99-115, Carnegie Mellon University, 1999. Available as: \nhttp:\/\/www.cs.cmu.edu\/~bryant\/pubdir\/cmu-cs-99-115.ps\n\n."},{"key":"40_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer-Aided Verification CAV\u2019 94","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, and D. L. Dill, \u201cAutomated verification of pipelined microprocessor control,\u201d Computer-Aided Verification CAV\u2019 94, D. L. Dill, ed., LNCS 818, Springer-Verlag, June, 1994, pp. 68\u201380."},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"W. Damm, A. Pnueli, and S. Ruah, \u201cHerbrand automata for hardware verification,\u201d 9th International Conference on Concurrency Theory CONCUR\u2019 98, Springer-Verlag, September, 1998.","DOI":"10.1007\/BFb0055616"},{"key":"40_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Computer-Aided Verification CAV\u2019 98","author":"A. Goel","year":"1998","unstructured":"A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal, \u201cBDD based procedures for a theory of equality with uninterpreted functions,\u201d Computer-Aided Verification CAV\u2019 98,A. J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June, 1998, pp. 244\u2013255."},{"key":"40_CR7","unstructured":"R. Hojati, A. Kuehlmann, S. German, and R. K. Brayton, \u201cValidity checking in the theory of equality with uinterpreted functions using finite instantiations,\u201d Unpublished paper presented at the International Workshop on Logic Synthesis, 1997."},{"issue":"2","key":"40_CR8","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson, and D. C. Oppen, \u201cFast decision procedures based on the congruence closure,\u201d J. ACM, Vol. 27, No.2 (1980), pp. 356\u2013364.","journal-title":"J. ACM"},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel, \u201cDeciding equality formulas by small-domain instantiations,\u201d Computer-Aided Verification CAV\u2019 99, this proceedings, 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"40_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-49519-3_3","volume-title":"Formal Methods in Computer-Aided Design FMCAD\u2019 98","author":"M.N. Velev","year":"1998","unstructured":"M.N. Velev, and R. E. Bryant, \u201cBit-level abstraction in the verification of pipelined microprocessors by correspondence checking.\u201d Formal Methods in Computer-Aided Design FMCAD\u2019 98, G. Gopalakrishnan and P. Windley, eds., LNCS 1522, Springer-Verlag, November, 1998, pp. 18\u201335."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:03:52Z","timestamp":1586138632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}