{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:29Z","timestamp":1725728969660},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_32","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T03:55:13Z","timestamp":1370318113000},"page":"443-449","source":"Crossref","is-referenced-by-count":1,"title":["bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR"],"prefix":"10.1007","author":[{"given":"Gergely","family":"Kov\u00e1sznai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proc. SMT 2012, pp. 44\u201355 (2012)","key":"32_CR1"},{"unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Proc. SMT 2010, Edinburgh, UK (2010)","key":"32_CR2"},{"key":"32_CR3","first-page":"33","volume-title":"BPR 2008","author":"R. Brummayer","year":"2008","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: bit-precise modelling of word-level problems for model checking. In: BPR 2008, pp. 33\u201338. ACM, New York (2008)"},{"issue":"3","key":"32_CR4","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci.\u00a021(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying equivalence of memories using a first order logic theorem prover. In: FMCAD 2009, pp. 128\u2013135 (2009)","key":"32_CR5","DOI":"10.1109\/FMCAD.2009.5351132"},{"unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: FMCAD 2010, pp. 137\u2013144 (2010)","key":"32_CR6"},{"unstructured":"$\\hbox{\\sc bv2epr}$\n                \u00a0project page, \n                  \n                    http:\/\/fmv.jku.at\/bv2epr\/","key":"32_CR7"},{"unstructured":"Hoder, K., Khasidashvili, Z., Korovin, K., Voronkov, A.: Preprocessing techniques for first-order clausification. In: FMCAD 2012, pp. 44\u201351 (2012)","key":"32_CR8"},{"doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: Proc. ICCAD 2009, pp. 13\u201320. IEEE (2009)","key":"32_CR9","DOI":"10.1145\/1687399.1687403"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T15:41:43Z","timestamp":1557762103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}