{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T05:24:51Z","timestamp":1738992291023,"version":"3.37.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,2,12]],"date-time":"2009-02-12T00:00:00Z","timestamp":1234396800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10009-009-0101-x","type":"journal-article","created":{"date-parts":[[2009,2,11]],"date-time":"2009-02-11T08:35:13Z","timestamp":1234341313000},"page":"95-104","source":"Crossref","is-referenced-by-count":13,"title":["An abstraction-based decision procedure for bit-vector arithmetic"],"prefix":"10.1007","volume":"11","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","published-online":{"date-parts":[[2009,2,12]]},"reference":[{"key":"101_CR1","doi-asserted-by":"crossref","unstructured":"Arons, T., Elster, E., Fix, L., Mador-Haim, S., Mishaeli, M., Shalev, J., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zuck, L.D.: Formal verification of backward compatibility of microcode. In: Proceedings of the Computer-Aided Verification (CAV\u201905). LNCS, vol. 2404, pp. 185\u2013198 (2005)","DOI":"10.1007\/11513988_20"},{"key":"101_CR2","unstructured":"Babic, D., Spear, F.H.: Proceedings of the SAT 2007 competition (2007)"},{"key":"101_CR3","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical report, Microsoft Research, Redmond (2005)"},{"key":"101_CR4","doi-asserted-by":"crossref","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)","DOI":"10.1145\/277044.277186"},{"key":"101_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Yhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"101_CR6","doi-asserted-by":"crossref","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proceedings of VLSI Design, pp. 741\u2013746. IEEE (2002)","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"101_CR7","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":"101_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907), pp. 358\u2013372 (2007)","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"101_CR9","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: 13th ACM Conference on Computer and Communications Security (CCS \u201906), pp. 322\u2013335. ACM, New York (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"101_CR10","doi-asserted-by":"crossref","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, Washington (2003)","DOI":"10.1145\/1119772.1119831"},{"key":"101_CR11","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: accurate theorem proving for program verification. In: Proceedings of CAV 2005, pp. 296\u2013300. Springer, Berlin (2005)","DOI":"10.1007\/11513988_30"},{"key":"101_CR12","doi-asserted-by":"crossref","unstructured":"Cyrluk, D., M\u00f6ller, M.O., Rue\u00df, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Computer-Aided Verification (CAV \u201997), pp. 60\u201371 (1997)","DOI":"10.1007\/3-540-63166-6_9"},{"key":"101_CR13","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Available at http:\/\/yices.csl.sri.com\/tool-paper.pdf (2006)"},{"key":"101_CR14","unstructured":"Ganesh, V., Berezin, S., Dill, D.: A decision procedure for fixed-width bit-vectors. Technical Report, Computer Science Department, Stanford University (2005)"},{"key":"101_CR15","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification (CAV \u201907), Berlin, Germany, July 2007. Springer, Berlin (2007)"},{"key":"101_CR16","unstructured":"Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD (2003)"},{"key":"101_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: Proceedings of DAC, pp. 118\u2013123 (2000)","DOI":"10.1145\/337292.337333"},{"key":"101_CR18","doi-asserted-by":"crossref","unstructured":"Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur R., Peled D. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201904). LNCS, vol. 3114, pp. 308\u2013320, Boston, MA, July 2004. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_24"},{"key":"101_CR19","unstructured":"Lahiri, S., Mehra, K.: Interpolant Based Decision Procedure for Quantifier-Free Presburger Arithmetic. Technical Report 2005-121, Microsoft Research (2005)"},{"key":"101_CR20","doi-asserted-by":"crossref","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS\u201903. Lect. Notes in Comp. Sci., vol. 2619 (2003)","DOI":"10.1007\/3-540-36577-X_2"},{"key":"101_CR21","unstructured":"MiniSat. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"101_CR22","unstructured":"Moscow, M.L.: http:\/\/www.dina.dk\/~sestoft\/mosml.html"},{"key":"101_CR23","doi-asserted-by":"crossref","unstructured":"Parthasarathy, G., Iyer, M.K., Cheng, K.-T., Wang, L.-C.: An efficient finite-domain constraint solver for circuits. In: Design Automation Conference (DAC), pp. 212\u2013217 (2004)","DOI":"10.1145\/996566.996628"},{"key":"101_CR24","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, volume 2. Springer-Verlag, 1983. Originally published 1970"},{"key":"101_CR25","unstructured":"UCLID verification system. http:\/\/www.cs.cmu.edu\/~uclid"},{"key":"101_CR26","doi-asserted-by":"crossref","unstructured":"Wedler, M., Stoffel, D., Kunz, W.: Normalization at the arithmetic bit level. In: Proceedings of DAC, pp. 457\u2013462. ACM Press, New York (2005)","DOI":"10.1145\/1065579.1065699"},{"key":"101_CR27","unstructured":"Wisconsin Safety Analyzer Project. http:\/\/www.cs.wisc.edu\/wisa"},{"key":"101_CR28","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using Boolean satisfiability. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL), pp. 351\u2013363 (2005)","DOI":"10.1145\/1047659.1040334"},{"key":"101_CR29","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: In Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), S. Margherita Ligure (2003)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0101-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0101-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0101-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T15:48:35Z","timestamp":1738943315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0101-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,12]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["101"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0101-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2009,2,12]]}}}