{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:42:00Z","timestamp":1777092120427,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642316111","type":"print"},{"value":"9783642316128","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_51","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T05:14:42Z","timestamp":1339996482000},"page":"493-495","source":"Crossref","is-referenced-by-count":2,"title":["Using Term Rewriting to Solve Bit-Vector Arithmetic Problems"],"prefix":"10.1007","author":[{"given":"Iago","family":"Abal","sequence":"first","affiliation":[]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"given":"Joe","family":"Hurd","sequence":"additional","affiliation":[]},{"given":"Jorge","family":"Sousa Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"51_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 System. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 76\u201387. Springer, Heidelberg (2003)"},{"key":"51_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"51_CR3","first-page":"73","volume-title":"Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification, PLPV 2009","author":"L. Erk\u00f6k","year":"2008","unstructured":"Erk\u00f6k, L., Matthews, J.: Pragmatic equivalence and safety checking in Cryptol. In: Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification, PLPV 2009, pp. 73\u201382. ACM, New York (2008)"},{"key":"51_CR4","unstructured":"Franzen, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph.D. thesis, University of Trento (March 2010)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2014 SAT 2012"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:08:40Z","timestamp":1777090120000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_51"}},"subtitle":["(Poster Presentation)"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}