{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:16:45Z","timestamp":1760044605676},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_53","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T07:00:16Z","timestamp":1245654016000},"page":"668-674","source":"Crossref","is-referenced-by-count":36,"title":["Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic"],"prefix":"10.1007","author":[{"given":"Susmit","family":"Jha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rhishikesh","family":"Limaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","volume-title":"Handbook of Satisfiability, ch. 8","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 8, vol.\u00a04. IOS Press, Amsterdam (2009)"},{"key":"53_CR2","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT\u00a04, 75\u201397 (2008)","journal-title":"JSAT"},{"key":"53_CR3","doi-asserted-by":"crossref","unstructured":"Brummayer, R.D., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Proc. of TACAS (March 2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"53_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., Cimatti, A., Franzen, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT(BV) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 547\u2013560. Springer, Heidelberg (2007)"},{"key":"53_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"53_CR6","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. Moura de","year":"2008","unstructured":"de Moura, L., Bjorner, 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":"53_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"53_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"53_CR9","first-page":"27","volume-title":"FMCAD 2007","author":"F. Hutter","year":"2007","unstructured":"Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: FMCAD 2007, pp. 27\u201334. IEEE Press, Los Alamitos (2007)"},{"key":"53_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73368-3_35","volume-title":"Computer Aided Verification","author":"P. Manolis","year":"2007","unstructured":"Manolis, P., Srinivasan, S.K., Vroon, D.: BAT Bit-level Analysis tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 303\u2013306. Springer, Heidelberg (2007)"},{"key":"53_CR11","doi-asserted-by":"crossref","unstructured":"Jain, H., Clarke, E.M.: Efficient SAT solving for Non-Clausal Formulas using DPLL, Graphs and Watched Cuts. In: 46th Design Automation Conference (2009)","DOI":"10.1145\/1629911.1630057"},{"key":"53_CR12","unstructured":"Pipatsrisawat, K., Darwiche, A.: Rsat 2.0: Sat solver description. Technical Report D\u2013153, Automated Reasoning Group, Computer Science Department, UCLA (2007)"},{"key":"53_CR13","unstructured":"SMT-COMP 2008 results, http:\/\/www.smtexec.org\/exec\/?jobs=311"},{"key":"53_CR14","unstructured":"SMT-LIB QF_BV logic, http:\/\/goedel.cs.uiowa.edu\/smtlib\/logics\/QF_BV.smt"},{"key":"53_CR15","unstructured":"SMT-LIB QF_BV benchmarks, http:\/\/combination.cs.uiowa.edu\/smtlib\/benchmarks.html"},{"key":"53_CR16","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification, release 70930. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"53_CR17","doi-asserted-by":"crossref","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. Technical Report, EECS Department, UC Berkeley (April 2009)","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"53_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N. Een","year":"2007","unstructured":"Een, N., Mishchenko, A., Sorensson, N.: Applying logic synthesis to speedup SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"53_CR19","volume-title":"Hacker\u2019s Delight","author":"H.S. Warren Jr.","year":"2003","unstructured":"Warren Jr., H.S.: Hacker\u2019s Delight. Addison Wesley, Reading (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T21:19:40Z","timestamp":1558387180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}