{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T14:37:28Z","timestamp":1789915048792,"version":"4.0.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_45","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"680-695","source":"Crossref","is-referenced-by-count":30,"title":["A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors"],"prefix":"10.1007","author":[{"given":"Liana","family":"Hadarean","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kshitij","family":"Bansal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"45_CR1","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular arithmetic decision procedure. Microsoft Research Redmond, Tech. Rep. TR-2005-114 (2005)"},{"issue":"3","key":"45_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.09.042","volume":"125","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., Donham, J.: Combining SAT methods with non-clausal decision heuristics. Electronic Notes in Theoretical Computer Science\u00a0125(3), 3\u201312 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"45_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C.W. Barrett","year":"2006","unstructured":"Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 512\u2013526. Springer, Heidelberg (2006)"},{"key":"45_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. In: SMT, vol.\u00a013 (2010)"},{"key":"45_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http:\/\/www.SMT-LIB.org"},{"key":"45_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: DAC, pp. 522\u2013527 (1998)","DOI":"10.21236\/ADA400400"},{"key":"45_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"45_CR8","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., Franz\u00e9n, 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":"45_CR9","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD 2009, pp. 13\u201320 (2009)","DOI":"10.1145\/1687399.1687403"},{"key":"45_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"45_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Computer Aided Verification","author":"D. Cyrluk","year":"1997","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 60\u201371. Springer, Heidelberg (1997)"},{"key":"45_CR12","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)"},{"key":"45_CR13","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., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"3","key":"45_CR14","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM\u00a052(3), 365\u2013473 (2005)","journal-title":"JACM"},{"key":"45_CR15","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. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"45_CR16","unstructured":"Franz\u00e9n, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD thesis, University of Trento (2010)"},{"key":"45_CR17","doi-asserted-by":"publisher","first-page":"1137","DOI":"10.1109\/TC.1983.1676174","volume":"32","author":"H. Fujiwara","year":"1983","unstructured":"Fujiwara, H., Member, S., Shimono, T., Member, S.: On the acceleration of test generation algorithms. IEEE Transactions on Computers\u00a032, 1137\u20131144 (1983)","journal-title":"IEEE Transactions on Computers"},{"key":"45_CR18","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.L.: 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":"45_CR19","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, ch. 4, pp. 131\u2013153. IOS Press (February 2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"issue":"6","key":"45_CR20","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract DPLL procedure to DPLL(T). JACM\u00a053(6), 937\u2013977 (2006)","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_45","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:01:55Z","timestamp":1746280915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}