{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:40Z","timestamp":1778498380773,"version":"3.51.4"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1023\/a:1021752130394","type":"journal-article","created":{"date-parts":[[2003,3,20]],"date-time":"2003-03-20T21:15:11Z","timestamp":1048194911000},"page":"39-58","source":"Crossref","is-referenced-by-count":26,"title":["Polynomial Formal Verification of Multipliers"],"prefix":"10.1007","volume":"22","author":[{"given":"Martin","family":"Keim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Molitor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5110195_CR1","doi-asserted-by":"crossref","unstructured":"A. Aziz, F. Balarin, S.-T. Cheng, R. Hojati, T. Kam, S.C. Krishnan, R.K. Ranjan, T.R. Shiple, V. Singhal, S. Tasiran, H.-Y. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, \u201cHSIS: A BDD-based environment for formal verification,\u201d 31nd Design Automation Conference, 1994, pp. 454\u2013459.","DOI":"10.1145\/196244.196467"},{"key":"5110195_CR2","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00292108","volume":"24","author":"B. Becker","year":"1987","unstructured":"B. Becker, \u201cAn easily testable optimal-time VLSI-multiplier,\u201d Acta Informatica, Vol. 24, pp. 363\u2013380, 1987.","journal-title":"Acta Informatica"},{"issue":"8","key":"5110195_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Trans. on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"5110195_CR4","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R.E. Bryant","year":"1991","unstructured":"R.E. Bryant, \u201cOn the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication,\u201d IEEE Trans. on Computers, Vol. 40, pp. 205\u2013213, 1991.","journal-title":"IEEE Trans. on Computers"},{"key":"5110195_CR5","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"R.E. Bryant, \u201cSymbolic boolean manipulation with ordered binary decision diagrams,\u201d ACM Comp. Surveys, Vol. 24, pp. 293\u2013318, 1992.","journal-title":"ACM Comp. Surveys"},{"key":"5110195_CR6","unstructured":"R.E."},{"key":"5110195_CR7","doi-asserted-by":"crossref","unstructured":"Bryant and Y. Chen, \u201cVerification of arithmetic functions with binary moment diagrams,\u201d Technical report CMU-CS\u201394\u2013160, Carnegie Mellon University, 1994.","DOI":"10.21236\/ADA281028"},{"key":"5110195_CR8","unstructured":"R.E."},{"key":"5110195_CR9","doi-asserted-by":"crossref","unstructured":"Bryant and Y. Chen, \u201cVerification of arithmetic circuits with binary moment diagrams,\u201d in 32nd Design Automation Conference, 1995, pp. 535\u2013541.","DOI":"10.1145\/217474.217583"},{"key":"5110195_CR10","unstructured":"J.R."},{"key":"5110195_CR11","doi-asserted-by":"crossref","unstructured":"Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, \u201cSequential circuit verification using symbolic model checking,\u201d in 27th Design Automation Conference, 1990, pp. 46\u201351.","DOI":"10.1145\/123186.123223"},{"key":"5110195_CR12","doi-asserted-by":"crossref","unstructured":"Y.-A. Chen and R.E. Bryant, \u201c*PHDD: An efficient graph representation for floating point circuit verification,\u201d in Int'l Conf. on CAD, 1997, pp. 2\u20137.","DOI":"10.1109\/ICCAD.1997.643251"},{"key":"5110195_CR13","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Fujita, and X. Zhao, \u201cHybrid decision diagrams\u2014Overcoming the limitations of MTBDDs and BMDs,\u201d Int'l Conf. on CAD, 1995, pp. 159\u2013163.","DOI":"10.1109\/ICCAD.1995.480007"},{"key":"5110195_CR14","doi-asserted-by":"crossref","unstructured":"R. Drechsler, B. Becker, and S. Ruppertz, \u201cK*BMDs: A new data structure for verification,\u201d in European Design & Test Conf., 1996, pp. 2\u20138.","DOI":"10.1109\/EDTC.1996.494118"},{"key":"5110195_CR15","unstructured":"R. Enders, \u201cNote on the complexity of binary moment diagram representations,\u201d in IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, 1995, pp. 191\u2013197."},{"key":"5110195_CR16","unstructured":"M. Fujita, H. Fujisawa, and N. Kawato, \u201cEvaluation and improvements of boolean comparison method based on binary decision diagrams,\u201d in International Conference on CAD, 1988, pp. 2\u20135."},{"key":"5110195_CR17","volume-title":"Logic Synthesis and Verification Algorithms","author":"G. Hachtel","year":"1996","unstructured":"G. Hachtel and F. Somezi, Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Dordrecht, 1996."},{"key":"5110195_CR18","doi-asserted-by":"crossref","unstructured":"K. Hamaguchi, A. Morita, and S. Yajma, \u201cEfficient construction of binary moment diagrams for verifying arithmetic circuits,\u201d in International Conference on CAD, 1995, pp. 78\u201382.","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"5110195_CR19","first-page":"155","volume-title":"VLSI'83","author":"W.K. Luk","year":"1983","unstructured":"W.K. Luk and J. Vuillemin, Recursive Implementation of Optimal Time VLSI Integer Multipliers. VLSI'83, F. Anceau, E.J. Aas (Eds.), pp. 155\u2013168, North Holland: Elsevier, 1983."},{"key":"5110195_CR20","unstructured":"S. Malik, A.R. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, \u201cLogic verification using binary decision diagrams in a logic synthesis environment,\u201d in Int'l Conf. on CAD, 1988, pp. 6\u20139."},{"key":"5110195_CR21","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/PGEC.1964.263830","volume":"EC-13","author":"C.S. Wallace","year":"1964","unstructured":"C.S. Wallace, \u201cA suggestion for a fast multiplier,\u201d IEE Trans. Electron. Computers, Vol. EC-13, pp. 14\u201317, 1964.","journal-title":"IEE Trans. Electron. Computers"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021752130394.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021752130394\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021752130394.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:11:32Z","timestamp":1754421092000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021752130394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["5110195"],"URL":"https:\/\/doi.org\/10.1023\/a:1021752130394","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}