{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:18:57Z","timestamp":1773656337416,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631668","type":"print"},{"value":"9783540691952","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_9","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:14:21Z","timestamp":1330280061000},"page":"60-71","source":"Crossref","is-referenced-by-count":24,"title":["An efficient decision procedure for the theory of fixed-sized bit-vectors"],"prefix":"10.1007","author":[{"given":"David","family":"Cyrluk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oliver","family":"M\u00f6ller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"9_CR2","first-page":"187","volume-title":"FMCAD '96, volume 1166 of Lecture Notes in Computer Science","author":"D. Dill","year":"1996","unstructured":"D. Dill, C. Barrett and J. Levitt. Validity Checking for Combinations of Theories with Equality. In M. Srivas, editor, FMCAD '96, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"9_CR3","first-page":"463","volume-title":"Proc. of CADE'96, volume 1104 of Lecture Notes in Artificial Intelligence","author":"D. Cyrluk","year":"1996","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak's Decision Procedure for Combination of Theories. In M. A. McRobbie and J. K. Slaney, editors, Proc. of CADE'96, volume 1104 of Lecture Notes in Artificial Intelligence, pages 463\u2013477, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"9_CR4","series-title":"Technical report, Universit\u00e4t Ulm, D-89069","volume-title":"An Efficient Decision Procedure for a Theory of Fixed-Sized Bitvectors with Composition and Extraction","author":"D. Cyrluk","year":"1996","unstructured":"D. Cyrluk, O. M\u00f6ller, and H. Rue\u00df. An Efficient Decision Procedure for a Theory of Fixed-Sized Bitvectors with Composition and Extraction. Technical report, Universit\u00e4t Ulm, D-89069 Ulm, Oberer Eselsberg, December 1996."},{"issue":"2","key":"9_CR5","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"H. Rue\u00df. Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study. In M.K. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, November 1996.","DOI":"10.1007\/BFb0031801"},{"issue":"1","key":"9_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"R.E. Shostak. Deciding Combinations of Theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"},{"key":"9_CR8","series-title":"International Series in Computer Science","first-page":"125","volume-title":"Applications of Formal Methods","author":"M.K. Srivas","year":"1995","unstructured":"M.K. Srivas and S.P. Miller. Formal Verification of the AAMP5 Microprocessor. In M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 7, pages 125\u2013180. Prentice Hall, Hemel Hempstead, UK, 1995."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:42:30Z","timestamp":1619559750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}