{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:10:29Z","timestamp":1737288629397,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660866"},{"type":"electronic","value":"9783540487548"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48754-9_1","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:20:56Z","timestamp":1184602856000},"page":"1-13","source":"Crossref","is-referenced-by-count":3,"title":["Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[]},{"given":"Steven","family":"German","sequence":"additional","affiliation":[]},{"given":"Miroslav N.","family":"Velev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"reference":[{"key":"1_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954."},{"key":"1_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u2019 96)","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt, \u201cValidity checking for combinations of theories with equality,\u201d Formal Methods in Computer-Aided Design (FMCAD\u2019 96), M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November, 1996, pp. 187\u2013201."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"S. Bose, and A. L. Fisher, \u201cVerifying Pipelined Hardware Using Symbolic Logic Simulation,\u201d International Conference on Computer Design (ICCD\u2019 89), 1989, pp. 217\u2013221.","DOI":"10.1109\/ICCD.1989.63359"},{"issue":"8","key":"1_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation\u201d, IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR5","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 electronically as: http:\/\/www.cs.cmu.edu\/~bryant\/pubdir\/cmu-cs-99-115.ps ."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, S. German, and M. N. Velev, \u201cExploiting positive equality in a logic of uninterpreted functions with equality,\u201d Computer-Aided Verification (CAV\u2019 99), 1999.","DOI":"10.1007\/3-540-48683-6_40"},{"key":"1_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","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":"1_CR8","doi-asserted-by":"crossref","unstructured":"J. R. Burch, \u201cTechniques for verifying superscalar microprocessors,\u201d 33rd Design Automation Conference (DAC\u2019 96), June, 1996, pp. 552\u2013557.","DOI":"10.1145\/240518.240623"},{"key":"1_CR9","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":"1_CR10","volume-title":"Computer Architecture: A Quantitative Approach","author":"J. L. Hennessy","year":"1996","unstructured":"J. L. Hennessy, and D. A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition Morgan-Kaufmann, San Francisco, 1996.","edition":"2nd edition"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. A. R. Hoare","year":"1972","unstructured":"C. A. R. Hoare, \u201cProof of Correctness of Data Representations,\u201d Acta Informatica Vol. 1, 1972, pp. 271\u2013281.","journal-title":"Acta Informatica"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"M. Kantrowitz, and L. M. Noack, \u201cI\u2019m Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor,\u201d 33rd Design Automation Conference (DAC\u2019 96), 1996, pp. 325\u2013330.","DOI":"10.1145\/240518.240580"},{"issue":"2","key":"1_CR13","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":"1_CR14","doi-asserted-by":"crossref","unstructured":"K. L. Nelson, A. Jain, and R. E. Bryant, \u201cFormal Verification of a Superscalar Execution Unit,\u201d 34th Design Automation Conference (DAC\u2019 97), June, 1997.","DOI":"10.1145\/266021.266055"},{"key":"1_CR15","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), 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","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 J. ACM, Vol. 26, No. 2 (1979), pp. 351\u2013360.","journal-title":"J. ACM"},{"issue":"5","key":"1_CR17","doi-asserted-by":"publisher","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 (Sept., 1990), pp. 52\u201364.","journal-title":"IEEE Software"},{"key":"1_CR18","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","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48754-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:53:40Z","timestamp":1737287620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48754-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660866","9783540487548"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48754-9_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}