{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T15:54:55Z","timestamp":1783612495178,"version":"3.55.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.23919\/fmcad.2017.8102237","type":"proceedings-article","created":{"date-parts":[[2017,11,9]],"date-time":"2017-11-09T21:49:00Z","timestamp":1510264140000},"page":"23-30","source":"Crossref","is-referenced-by-count":55,"title":["Column-wise verification of multipliers using computer algebra"],"prefix":"10.23919","author":[{"given":"Daniela","family":"Ritirc","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manuel","family":"Kauers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","first-page":"535","article-title":"Verification of arithmetic circuits with binary moment diagrams","author":"chen","year":"1995","journal-title":"DAC"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031797"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744925"},{"key":"ref13","author":"cox","year":"1997","journal-title":"Ideals Varieties and Algorithms"},{"key":"ref14","author":"decker","year":"2016","journal-title":"Singular 4-1–0"},{"key":"ref15","first-page":"61","article-title":"Effective preprocessing in SAT through variable and clause elimination","volume":"3569","author":"e\u00e9n","year":"2005","journal-title":"SAT"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1093\/ietfec\/e89-a.12.3500"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9239-9"},{"key":"ref18","first-page":"345","article-title":"An ideal-theoretic approach to work problems and unification problems over finitely presented commutative algebras","volume":"202","author":"kandri-rody","year":"1985","journal-title":"RTA"},{"key":"ref19","author":"koren","year":"2001","journal-title":"Computer Arithmetic Algorithms"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2547898"},{"key":"ref4","first-page":"65","article-title":"Collection of combinational arithmetic miters submitted to the SAT Competition 2016","author":"biere","year":"2016","journal-title":"SAT Competition 2016 volume B-2016–1 of Department of Computer Science Series of Publications B"},{"key":"ref27","year":"2016","journal-title":"Wolfram Research Inc Mathematica"},{"key":"ref3","year":"2017","journal-title":"ABC A System for Sequential Synthesis and Verification"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref5","author":"biere","year":"2016","journal-title":"Weaknesses of CDCL solvers"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"7763","DOI":"10.4249\/scholarpedia.7763","volume":"5","author":"buchberger","year":"2010","journal-title":"Scholarpedia"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/s100090100037","article-title":"Verification of arithmetic circuits using binary moment diagrams","volume":"3","author":"bryant","year":"2001","journal-title":"STTT"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_13"},{"key":"ref9","first-page":"169","author":"chen","year":"2001","journal-title":"Equivalence checking of integer multipliers"},{"key":"ref1","first-page":"452","article-title":"Complexity of testing whether a polynomial ideal is nontrivial","author":"agnarsson","year":"1984","journal-title":"Third MACSYMA User's Conference"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref22","first-page":"53","article-title":"Boolector 2.0 system description","volume":"9","author":"niemetz","year":"2014","journal-title":"JSAT"},{"key":"ref21","first-page":"1409","article-title":"Efficient Gröbner basis reductions for formal verification of Galois field arithmetic circuits","volume":"32","author":"lv","year":"2013","journal-title":"IEEE TCAD"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"1048","DOI":"10.3850\/9783981537079_0248","article-title":"Formal verification of integer multipliers by combining Gröbner basis with logic reduction","author":"sayed-ahmed","year":"2016","journal-title":"DATE"},{"key":"ref23","first-page":"152:1","article-title":"Equivalence verification of large Galois field arithmetic circuits using word-level abstraction via Gröbner bases","author":"pruss","year":"2014","journal-title":"DAC"},{"key":"ref26","first-page":"473","article-title":"An algebraic approach for proving data correctness in arithmetic data paths","volume":"5123","author":"wienand","year":"2008","journal-title":"CAV"},{"key":"ref25","first-page":"169","article-title":"Equivalence checking using Gröbner bases","author":"sayed-ahmed","year":"2016","journal-title":"FMCAD"}],"event":{"name":"2017 Formal Methods in Computer-Aided Design (FMCAD)","location":"Vienna","start":{"date-parts":[[2017,10,2]]},"end":{"date-parts":[[2017,10,6]]}},"container-title":["2017 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8093672\/8102222\/08102237.pdf?arnumber=8102237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T13:53:27Z","timestamp":1603288407000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8102237\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":28,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2017.8102237","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}