{"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":1773656337780,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540651918","type":"print"},{"value":"9783540495192","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_4","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"36-48","source":"Crossref","is-referenced-by-count":16,"title":["Solving Bit-Vector Equations"],"prefix":"10.1007","author":[{"given":"M. Oliver","family":"M\u00f6ller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\\","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"C.W. Barrett, D.L. Dill, and J.R. Levitt. A Decision Procedure for Bit-Vector Arithmetic. In Proceedings of the 35th Design Automation Conference, June 1998. San Francisco, CA.","DOI":"10.21236\/ADA400400"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00d8rner and M.C. Pichora. Deciding Fixed and Non-Fixed Size Bit-Vectors. volume 1384 of Lecture Notes in Computer Science LNCS, pages 376\u2013392, Heidelberg-New York-Berlin, April 1998. Springer.","DOI":"10.1007\/BFb0054184"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak\u2019s Decision Procedure for Combinations of Theories. In A. cRobbie and J. K. Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-96), volume 1104 of LNAI, pages 463\u2013477, Berlin;Heidelberg;New York, 1996. Springer.","DOI":"10.1007\/3-540-61511-3_107"},{"key":"4_CR4","unstructured":"D. Cyrluk, M.O. M\u00f6ller, and H. Rue\\ An Efficient Decision Procedure for a Theory of Fixed-Size Bitvectors with Composition and Extraction. Ulmer Informatik-Berichte 96-08, Fakult\u00c4t f\u00fcr Informatik, Universit\u00c4t Ulm, 1996."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Computer Aided Verification. 9th International Conference (CAV97). Haifa, Israel","author":"D. Cyrluk","year":"1997","unstructured":"D. Cyrluk, M.O. M\u00f6ller, and H. Rueff. An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. In O. Grumberg, editor, Computer Aided Verification. 9th International Conference (CAV97). Haifa, Israel, June 22\u201325, 1997: Proceedings, volume 1254 of Lecture Notes in Computer Science LNCS, pages 60\u201371, Berlin-Heidelberg-New York, 1997. Springer."},{"key":"4_CR6","unstructured":"A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous Rigid E-Unification is not so Simple. UPMAIL Technical Report 104, Uppsala University, Computing Science Department, 1995."},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1090\/S0002-9947-1978-0469886-1","volume":"235","author":"L. Lipshitz","year":"1978","unstructured":"L. Lipshitz. The Diophantine Problem for Addition and Divisibility. Transactions of the American Mathematical Society, 235:271\u2013283, January 1978.","journal-title":"Transactions of the American Mathematical Society"},{"issue":"1","key":"4_CR8","first-page":"41","volume":"33","author":"L. Lipshitz","year":"1981","unstructured":"L. Lipshitz. Some Remarks on the Diophantine Problem for Addition and Divisibility. Bull. Soc. Math. Belg. S\u2019er. B, 33(1):41\u201352, 1981.","journal-title":"Bull. Soc. Math. Belg. S\u2019er. B"},{"key":"4_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings of Word Equations and Related Topics (IWWERT\u2019 90)","author":"G. S. Makanin","year":"1992","unstructured":"G. S. Makanin. Investigations on equations in a free group. In K.U. Schulz, editor, Proceedings of Word Equations and Related Topics (IWWERT\u2019 90), volume 572 of LNCS, pages 1\u201311, Berlin;Heidelberg;New York, 1992. Springer."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"M.O. M\u00f6ller. Solving Bit-Vector Equations A Decision Procedure for Hardware Verification, 1998. Diploma Thesis, available from http:\/\/www.informatik.uni-ulm.de\/~ki,Bitvector","DOI":"10.1007\/3-540-49519-3_4"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"W. Plandowski and W. Rytter. Application of Lempel-Ziv Encodings to the Solution of Words Equations. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, ICALP\u201998, pages 731\u2013742, July 1998. Aalborg, Denmark.","DOI":"10.1007\/BFb0055097"},{"issue":"1","key":"4_CR12","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":"4_CR13","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","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:00Z","timestamp":1556906340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]}}}