{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:09:33Z","timestamp":1746158973871},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_16","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T07:14:55Z","timestamp":1465542895000},"page":"249-266","source":"Crossref","is-referenced-by-count":21,"title":["Deciding Bit-Vector Formulas with mcSAT"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Zelji\u0107","sequence":"first","affiliation":[]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-12002-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bardin","year":"2010","unstructured":"Bardin, S., Herrmann, P., Perroud, F.: An alternative to SAT-based approaches for bit-vectors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 84\u201398. Springer, Heidelberg (2010)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-642-31424-7_16","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2012","unstructured":"Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing abstraction failure for separation logic\u2013based analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 155\u2013173. Springer, Heidelberg (2012)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC (1999)","DOI":"10.1109\/DAC.1999.781333"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BFb0054184","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"NS Bj\u00f8rner","year":"1998","unstructured":"Bj\u00f8rner, N.S., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 376\u2013392. Springer, Heidelberg (1998)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-642-25379-9_15","volume-title":"Certified Programs and Proofs","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 183\u2013198. Springer, Heidelberg (2011)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: sat-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD. ACM (2009)","DOI":"10.1145\/1687399.1687403"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, M.O., Rue\u00df, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 60\u201371. Springer, Heidelberg (1997)"},{"issue":"6188","key":"16_CR16","doi-asserted-by":"crossref","first-page":"1156","DOI":"10.1126\/science.1248882","volume":"344","author":"SJ Dunn","year":"2014","unstructured":"Dunn, S.J., Martello, G., Yordanov, B., Emmott, S., Smith, A.: Defining an essential transcriptional factor program for naive pluripotency. Science 344(6188), 1156\u20131160 (2014)","journal-title":"Science"},{"key":"16_CR17","unstructured":"Dutertre, B.: System description: Yices 1.0.10. In: SMT-COMP 2007 (2007)"},{"key":"16_CR18","unstructured":"Froehlich, A., Kovasznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: SMT Workshop (2013)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-642-38536-0_33","volume-title":"Computer Science \u2013 Theory and Applications","author":"A Fr\u00f6hlich","year":"2013","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 378\u2013390. Springer, Heidelberg (2013)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"16_CR21","unstructured":"Griggio, A.: Effective word-level interpolation for software verification. In: FMCAD. FMCAD Inc. (2011)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","volume-title":"Computer Aided Verification","author":"L Hadarean","year":"2014","unstructured":"Hadarean, L., Bansal, K., Jovanovi\u0107, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680\u2013695. Springer, Heidelberg (2014)"},{"issue":"1","key":"16_CR23","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovic","year":"2013","unstructured":"Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning 51(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: SMT. EPiC Series, vol. 20. EasyChair (2013)","DOI":"10.1007\/978-3-642-38536-0_33"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-662-44465-8_41","volume-title":"Mathematical Foundations of Computer Science 2014","author":"G Kov\u00e1sznai","year":"2014","unstructured":"Kov\u00e1sznai, G., Veith, H., Fr\u00f6hlich, A., Biere, A.: On the complexity of symbolic verification and decision problems in bit-vector logic. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014, Part II. LNCS, vol. 8635, pp. 481\u2013492. Springer, Heidelberg (2014)"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Kroening, D.: Computing over-approximations with bounded model checking. In: BMC Workshop, vol. 144, January 2006","DOI":"10.1016\/j.entcs.2005.07.021"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-49519-3_4","volume-title":"Formal Methods in Computer-Aided Design","author":"MO M\u00f6ller","year":"1998","unstructured":"M\u00f6ller, M.O., Rue\u00df, H.: Solving bit-vector equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 36\u201348. Springer, Heidelberg (1998)"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"issue":"6","key":"16_CR31","doi-asserted-by":"crossref","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 Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (1970), translated from Russian: Zapiski Nauchnykh Seminarov LOMI 8 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Wille, R., Fey, G., Gro\u00dfe, D., Eggersgl\u00fc\u00df, S., Drechsler, R.: SWORD: a SAT like prover using word level information. In: International Conference on Very Large Scale Integration of System-on-Chip (VLSI-SoC 2007). IEEE (2007)","DOI":"10.1109\/VLSISOC.2007.4402478"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-642-38088-4_6","volume-title":"NASA Formal Methods","author":"B Yordanov","year":"2013","unstructured":"Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 78\u201392. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T10:09:33Z","timestamp":1568023773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}