{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:54:31Z","timestamp":1755838471004},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_24","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"340-355","source":"Crossref","is-referenced-by-count":13,"title":["Fine Grained SMT Proofs for the Theory of\u00a0Fixed-Width Bit-Vectors"],"prefix":"10.1007","author":[{"given":"Liana","family":"Hadarean","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"24_CR2","unstructured":"Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: All about Proofs, Proofs for All, pp. 23\u201344 (2015)"},{"key":"24_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2015). \n                    www.SMT-LIB.org"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Conference on Computer Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_18"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-25379-9_13","volume-title":"Certified Programs and Proofs","author":"F Besson","year":"2011","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 151\u2013166. Springer, Heidelberg (2011)"},{"issue":"1","key":"24_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Bouton, T., Caminha, D., De Oliveira, B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Conference on Automated Deduction (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"24_CR10","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. 5505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Chen, J., Chugh, R., Swamy, N.: Type-preserving compilation of end-to-end verification of security enforcement. In: Programming Language Design and Implementation (2010)","DOI":"10.1145\/1806596.1806643"},{"key":"24_CR12","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"24_CR14","unstructured":"Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Workshop on Satisfiability Modulo Theories (2008)"},{"key":"24_CR15","unstructured":"Griggio, A.: Effective word-level interpolation for software verification. In: Formal Methods in Computer-Aided Design (2011)"},{"key":"24_CR16","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":"24_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: SeL4: formal verification of an OS kernel. In: Symposium on Operating Systems Principles (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"24_CR20","unstructured":"S. Lescuyer and S. Conchon. A Reflexive Formalization of a SAT Solver in Coq. In Theorem Proving in Higher Order Logics, 2008"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: a case study combining HOL-Light and CVC lite. In: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005) (2006)","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Moskal","year":"2008","unstructured":"Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486\u2013500. Springer, Heidelberg (2008)"},{"issue":"6","key":"24_CR23","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 davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Workshop on Satisfiability Modulo Theories (2009)","DOI":"10.1145\/1670412.1670414"},{"key":"24_CR25","unstructured":"Reynolds, A., Hadarean, L., Tinelli, C., Ge, Y., Stump, A., Barrett, C.: Comparing proof systems for linear real arithmetic with LFSC. In: Workshop on Satisfiability Modulo Theories (2010)"},{"key":"24_CR26","unstructured":"Reynolds, A., Tinelli, C., Hadarean, L.: Certified interpolant generation for EUF. In: Workshop on Satisfiability Modulo Theories (2011)"},{"key":"24_CR27","volume-title":"Logic: Form and Function: The Mechanization of Deductive Reasoning","author":"JA Robinson","year":"1980","unstructured":"Robinson, J.A.: Logic: Form and Function: The Mechanization of Deductive Reasoning. Elsevier, New York (1980)"},{"issue":"1","key":"24_CR28","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"42","author":"A Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1), 91\u2013118 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014)"},{"key":"24_CR30","unstructured":"Van, A.: Gelder. \n                    http:\/\/users.soe.ucsc.edu\/avg\/ProofChecker\/ProofChecker-fileformat.txt"},{"key":"24_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:25:27Z","timestamp":1559330727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}