{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T09:02:23Z","timestamp":1774602143002,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_28","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"358-372","source":"Crossref","is-referenced-by-count":55,"title":["Deciding Bit-Vector Arithmetic with Abstraction"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bryan","family":"Brady","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","first-page":"193","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., et al.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"28_CR2","first-page":"308","volume-title":"Proceedings of ASP-DAC 2003","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Proceedings of ASP-DAC 2003, pp. 308\u2013311. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using Boolean satisfiability. In: Proc. 32nd ACM Symposium on Principles of Programming Languages (POPL), pp. 351\u2013363 (2005)","DOI":"10.1145\/1040305.1040334"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","first-page":"185","volume-title":"Computer Aided Verification","author":"M.Y. Vardi","year":"2005","unstructured":"Vardi, M.Y., et al.: Formal Verification of Backward Compatibility of Microcode. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 185\u2013198. Springer, Heidelberg (2005)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., et al.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. McMillan","year":"2003","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/11513988_30","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 296\u2013300. Springer, Heidelberg (2005)"},{"key":"28_CR8","unstructured":"Berezin, S., Ganesh, V., Dill, D.: A decision procedure for fixed-width bit-vectors. Technical report, Computer Science Department, Stanford University (2005)"},{"key":"28_CR9","first-page":"457","volume-title":"Proc.\u00a0DAC","author":"M. Wedler","year":"2005","unstructured":"Wedler, M., Stoffel, D., Kunz, W.: Normalization at the arithmetic bit level. In: Proc.\u00a0DAC, pp. 457\u2013462. ACM Press, New York (2005)"},{"key":"28_CR10","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1145\/1180405.1180445","volume-title":"13th ACM Conference on Computer and Communications Security (CCS \u201906)","author":"C. Cadar","year":"2006","unstructured":"Cadar, C., et al.: EXE: Automatically generating inputs of death. In: 13th ACM Conference on Computer and Communications Security (CCS \u201906), pp. 322\u2013335. ACM, New York (2006)"},{"key":"28_CR11","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (2006), Available at \n                    \n                      http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"28_CR12","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.\u00a01254, pp. 60\u201371. Springer, Heidelberg (1997)"},{"key":"28_CR13","first-page":"522","volume-title":"Proceedings of DAC\u201998","author":"C.W. Barrett","year":"1998","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proceedings of DAC\u201998, pp. 522\u2013527. ACM Press, New York (1998)"},{"key":"28_CR14","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical report, Microsoft Research, Redmond (2005)"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proceedings of VLSI Design, pp. 741\u2013746 (2002)","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Parthasarathy, G., et al.: An efficient finite-domain constraint solver for circuits. In: Design Automation Conference (DAC), pp. 212\u2013217 (2004)","DOI":"10.1145\/996566.996628"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Huang, C.Y., Cheng, K.T.: Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In: Proc. DAC, pp. 118\u2013123 (2000)","DOI":"10.1145\/337292.337333"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Gupta, A., et al.: Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD (2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"28_CR19","unstructured":"Lahiri, S., Mehra, K.: Interpolant based decision procedure for quantifier-free Presburger arithmetic. Technical Report 2005-121, Microsoft Research (2005)"},{"key":"28_CR20","volume-title":"Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, vol. 2","author":"G. Tseitin","year":"1983","unstructured":"Tseitin, G.: On the complexity of proofs in poropositional logics. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, vol. 2 (Originally published 1970). Springer, Heidelberg (1983)"},{"key":"28_CR21","unstructured":"zChaff: \n                    \n                      http:\/\/www.ee.princeton.edu\/~chaff\/zchaff.php"},{"key":"28_CR22","unstructured":"MiniSat: \n                    \n                      http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"28_CR23","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable Boolean formulas. In: Proceedings of SAT\u00a003 (2003)"},{"key":"28_CR24","unstructured":"UCLID verification system: \n                    \n                      http:\/\/www.cs.cmu.edu\/~uclid"},{"key":"28_CR25","unstructured":"MoscowML: \n                    \n                      http:\/\/www.dina.dk\/~sestoft\/mosml.html"},{"key":"28_CR26","unstructured":"Bryant, R.E.: Term-level verification of a pipelined CISC microprocessor. Technical Report CMU-CS-05-195, Computer Science Department, Carnegie Mellon University (2005)"},{"key":"28_CR27","unstructured":"Wisconsin Safety Analyzer Project: \n                    \n                      http:\/\/www.cs.wisc.edu\/wisa"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:45Z","timestamp":1605763005000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_28","relation":{},"subject":[]}}