{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T19:51:51Z","timestamp":1771530711326,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_8","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"131-150","source":"Crossref","is-referenced-by-count":3,"title":["Matching Multiplications in Bit-Vector Formulas"],"prefix":"10.1007","author":[{"given":"Supratik","family":"Chakraborty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Jain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC 2003, pp. 368\u2013371. ACM Press (2003)","DOI":"10.21236\/ADA461052"},{"key":"8_CR2","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, Berlin (2009). doi: 10.1007\/978-3-642-00768-2_16"},{"key":"8_CR3","unstructured":"EBMC. http:\/\/www.cprover.org\/ebmc\/"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Kroening, 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, Berlin (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427\u2013443. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_32"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi: 10.1007\/11804192_17"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"882","DOI":"10.1007\/11564751_120","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"Y Naveh","year":"2005","unstructured":"Naveh, Y., Emek, R.: Random stimuli generation for functional hardware verification as a CP application. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, p. 882. Springer, Heidelberg (2005). doi: 10.1007\/11564751_120"},{"key":"8_CR8","unstructured":"Naveh, Y., Rimon, M., Jaeger, I., Katz, Y., Vinov, M., Marcus, E., Shurek, G.: Constraint-based random stimuli generation for hardware verification. In: Proceedings of AAAI, pp. 1720\u20131727 (2006)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, 12\u201315 June 2005, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, Lisbon, Portugal, 5\u20139 September 2005, pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"8_CR11","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885 (2009)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L Moura","year":"2013","unstructured":"Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15\u201344. Springer, Berlin (2013). doi: 10.1007\/978-3-642-36675-8_2"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-319-21668-3_8","volume-title":"Computer Aided Verification","author":"S Chakraborty","year":"2015","unstructured":"Chakraborty, S., Khasidashvili, Z., Seger, C.-J.H., Gajavelly, R., Haldankar, T., Chhatani, D., Mistry, R.: Word-level symbolic trajectory evaluation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 128\u2013143. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21668-3_8"},{"key":"8_CR14","unstructured":"Long multiplication. https:\/\/en.wikipedia.org\/wiki\/Multiplication_algorithm#Long_multiplication"},{"key":"8_CR15","unstructured":"Booth\u2019s multiplication algorithm. https:\/\/en.wikipedia.org\/wiki\/Booth\u2019s_multiplication_algorithm"},{"issue":"1","key":"8_CR16","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/PGEC.1964.263830","volume":"13","author":"CS Wallace","year":"1964","unstructured":"Wallace, C.S.: A suggestion for a fast multiplier. IEEE Trans. Electron. Comput. 13(1), 14\u201317 (1964)","journal-title":"IEEE Trans. Electron. Comput."},{"key":"8_CR17","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","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-22110-1_14"},{"issue":"5","key":"8_CR19","doi-asserted-by":"crossref","first-page":"586","DOI":"10.1109\/TCAD.2004.826548","volume":"23","author":"D Stoffel","year":"2004","unstructured":"Stoffel, D., Kunz, W.: Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE Trans. CAD Integr. Circuits Syst. 23(5), 586\u2013597 (2004)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Yu, C., Ciesielski, M.J.: Automatic word-level abstraction of datapath. In: IEEE International Symposium on Circuits and Systems, ISCAS 2016, Montr\u00e9al, QC, Canada, 22\u201325 May 2016, pp. 1718\u20131721 (2016)","DOI":"10.1109\/ISCAS.2016.7538899"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: Design, Automation and Test in Europe, DATE 2009, Nice, France, 20\u201324 April 2009, pp. 196\u2013201 (2009)","DOI":"10.1109\/DATE.2009.5090657"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Tsiskaridze, N., Pasricha, K., Reisman, D., Susnea, A., Malik, S.: Reverse engineering digital circuits using functional analysis. In: Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18\u201322, 2013, pp. 1277\u20131280 (2013)","DOI":"10.7873\/DATE.2013.264"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Li, W., Gasc\u00f3n, A., Subramanyan, P., Tan, W.Y., Tiwari, A., Malik, S., Shankar, N., Seshia, S.A.: Wordrev: Finding word-level structures in a sea of bit-level gates. In: 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2013, Austin, TX, USA, 2\u20133 June 2013, pp. 67\u201374 (2013)","DOI":"10.1109\/HST.2013.6581568"},{"key":"8_CR24","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008)","edition":"1"},{"key":"8_CR25","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"issue":"5","key":"8_CR26","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR27","unstructured":"Bayardo, R.J., Jr., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 1997, IAAI 1997, 27\u201331 July 1997, Providence, Rhode Island, pp. 203\u2013208 (1997)"},{"key":"8_CR28","unstructured":"Chakraborty, S., Gupta, A., Jain, R.: Matching multiplications in bit-vector formulas. https:\/\/arxiv.org\/abs\/1611.10146"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Chen, Y.-A.: Verification of arithmetic circuits with binary moment diagrams. In: DAC, pp. 535\u2013541 (1995)","DOI":"10.1145\/217474.217583"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed, A., Gro\u00dfe, D., K\u00fchne, U., Soeken, M., Drechsler, R.: Formal verification of integer multipliers by combining gr\u00f6bner basis with logic reduction. In: 2016 Design, Automation & Test in Europe Conference & Exhibition, DATE 2016, Dresden, Germany, 14\u201318 March 2016, pp. 1048\u20131053 (2016)","DOI":"10.3850\/9783981537079_0248"},{"key":"8_CR31","unstructured":"HECTOR. http:\/\/www.synopsys.com\/Tools\/Verification\/FunctionalVerification\/Pages\/hector.aspx"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T11:09:41Z","timestamp":1568718581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}