{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:37:16Z","timestamp":1773952636101,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_45","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"473-486","source":"Crossref","is-referenced-by-count":26,"title":["An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths"],"prefix":"10.1007","author":[{"given":"Oliver","family":"Wienand","sequence":"first","affiliation":[]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[]},{"given":"Gert-Martin","family":"Greuel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","doi-asserted-by":"crossref","unstructured":"Kroening, D., Seshia, S.A.: Formal verification at higher levels of abstraction. In: Proc. International Conference on Computer-Aided Design (ICCAD) (2007)","DOI":"10.1109\/ICCAD.2007.4397326"},{"key":"45_CR2","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proc. International Design Automation Conference (2003)","DOI":"10.1145\/775832.775945"},{"key":"45_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"45_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered smt(\n                    \n                      \n                    \n                    $\\mathcal\\{BV\\}$\n                  ) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 547\u2013560. Springer, Heidelberg (2007)"},{"key":"45_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L.M. Moura de","year":"2007","unstructured":"de Moura, L.M., Bjoerner, N.: Efficient e-matching for smt solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"45_CR6","unstructured":"Spear, \n                    \n                      http:\/\/www.cs.ubc.ca\/~babic\/index.htm"},{"key":"45_CR7","doi-asserted-by":"crossref","unstructured":"Shekhar, N., Kalla, P., Enescu, F., Gopalakrishnan, S.: Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra. In: Proc. International Conference on Computer-Aided Design (ICCAD) (2005)","DOI":"10.1109\/ICCAD.2005.1560081"},{"key":"45_CR8","doi-asserted-by":"crossref","unstructured":"Shekhar, N., Kalla, P., Enescu, F.: Equivalence verification of arithmetic datapath with multiple word-length operands. In: Proc. International Conference on Design, Automation and Test in Europe (DATE) (2006)","DOI":"10.1109\/DATE.2006.244150"},{"issue":"7","key":"45_CR9","doi-asserted-by":"publisher","first-page":"1320","DOI":"10.1109\/TCAD.2006.888277","volume":"26","author":"N. Shekhar","year":"2007","unstructured":"Shekhar, N., Kalla, P., Enescu, F.: Equivalence verification of polynomial datapaths using ideal membership testing. IEEE Transactions on Computer-Aided Design\u00a026(7), 1320\u20131330 (2007)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"45_CR10","doi-asserted-by":"crossref","unstructured":"Watanabe, Y., Homma, N., Aoki, T., Higuchi, T.: Application of symbolic computer algebra to arithmetic circuit verification. In: Proc. International Conference on Computer Design (ICCD), pp. 25\u201332 (October 2007)","DOI":"10.1109\/ICCD.2007.4601876"},{"issue":"11","key":"45_CR11","doi-asserted-by":"publisher","first-page":"1909","DOI":"10.1109\/TCAD.2007.906458","volume":"26","author":"M. Wedler","year":"2007","unstructured":"Wedler, M., Stoffel, D., Brinkmann, R., Kunz, W.: A normalization method for arithmetic data-path verification. IEEE Transactions on Computer-Aided Design\u00a026(11), 1909\u20131922 (2007)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"45_CR12","unstructured":"Adams, W., Loustaunau, P.: An introduction to Gr\u00f6bner bases. (Graduate studies in mathematics) AMS (2003)"},{"key":"45_CR13","first-page":"705","volume-title":"A SINGULAR Introduction to Commutative Algebra","author":"G.M. Greuel","year":"2007","unstructured":"Greuel, G.M., Pfister, G.: A SINGULAR Introduction to Commutative Algebra, 2nd edn., 705 pages. Springer, Heidelberg (2007)","edition":"2"},{"key":"45_CR14","unstructured":"Wienand, O.: The Gr\u00f6bner basis of the ideal of vanishing polynomials (2007) arXiv: arXiv:0709.2978v1 [math.AC]"},{"key":"45_CR15","unstructured":"Brickenstein, M., Dreyer, A., Greuel, G.M., Wedler, M., Wienand, O.: New developments in the theory of Gr\u00f6bner bases and applications to formal verification. Journal of Pure and Applied Algebra (accepted for publication)"},{"key":"45_CR16","unstructured":"Greuel, G.M., Pfister, G., Sch\u00f6nemann, H.: Singular 3.0.4. - A Computer Algebra System for Polynomial Computations. Centre for Computer Algebra, University of Kaiserslautern (2007), \n                    \n                      http:\/\/www.singular.uni-kl.de"},{"key":"45_CR17","unstructured":"Onespin Solutions GmbH Munich, Germany, \n                    \n                      www.onespin.com"},{"issue":"3-4","key":"45_CR18","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1006\/jsco.1996.0125","volume":"24","author":"W. Bosma","year":"1997","unstructured":"Bosma, W., Cannon, J., Playoust, C.: The MAGMA algebra system I: the user language. J. Symb. Comput.\u00a024(3-4), 235\u2013265 (1997)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:22:01Z","timestamp":1620015721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}