{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,15]],"date-time":"2026-10-15T16:39:11Z","timestamp":1792082351195,"version":"4.4.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894250","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"28-36","source":"Crossref","is-referenced-by-count":81,"title":["Verifying Large Multipliers by Combining SAT and Computer Algebra"],"prefix":"10.23919","author":[{"given":"Daniela","family":"Kaufmann","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","doi-asserted-by":"publisher","DOI":"10.1093\/ietfec\/e89-a.12.3500"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0399"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-018-00329-2"},{"key":"ref13","article-title":"Arithmetic Verification Problems Submitted to the SAT Race 2019","author":"kaufmann","year":"2019","journal-title":"In Proc of SAT Race 2019"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref15","article-title":"Effective computation of strong Gröbner bases over Euclidean domains","volume":"56","author":"lichtblau","year":"2013","journal-title":"Illinois Journal of Mathematics"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2259540"},{"key":"ref17","first-page":"129","author":"mahzoon","year":"2018","journal-title":"PolyCleaner clean your polynomials before backward rewriting to verify million-gate multipliers"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317898"},{"key":"ref19","author":"mahzoon","year":"2019","journal-title":"Multiplier Generator GenMul"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2017.2772854"},{"key":"ref4","author":"buchberger","year":"1965","journal-title":"Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2808457"},{"key":"ref3","article-title":"CaDiCaL at the SAT Race 2019","author":"biere","year":"2019","journal-title":"In Proc of SAT Race 2019"},{"key":"ref6","author":"decker","year":"2016"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2912944"},{"key":"ref8","first-page":"1","article-title":"Proofs for Satisfiability Problems","volume":"55","author":"heule","year":"2015","journal-title":"All about Proofs Proofs for All"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0913-3"},{"key":"ref9","author":"hirsch","year":"2005","journal-title":"Report on the Mixed Boolean-Algebraic Solver 1"},{"key":"ref1","author":"artin","year":"1991","journal-title":"Algebra"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/978-3-319-96145-3_32","article-title":"Btor2, BtorMC and Boolector 3.0","volume":"10981","author":"niemetz","year":"2018","journal-title":"CAV 93 Computer-aided Verification"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102237"},{"key":"ref21","author":"parhami","year":"2000","journal-title":"Computer Arithmetic - Algorithms and Hardware Designs"},{"key":"ref24","first-page":"422","article-title":"DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs","volume":"8561","author":"wetzler","year":"2014","journal-title":"Conference on Theory and Application of Satisfiability Testing"},{"key":"ref23","first-page":"61","article-title":"A Practical Polynomial Calculus for Arithmetic Circuit Verification","author":"ritirc","year":"2018","journal-title":"3rd International Workshop on Satisfiability Checking and Symbolic Computation (SC2’18)"},{"key":"ref26","year":"2016","journal-title":"Inc Mathematica"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/978-3-540-70545-1_45","article-title":"An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths","volume":"5123","author":"wienand","year":"2008","journal-title":"CAV 93 Computer-aided Verification"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","location":"San Jose, CA, USA","start":{"date-parts":[[2019,10,22]]},"end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894250.pdf?arnumber=8894250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T22:45:07Z","timestamp":1598222707000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894250\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":28,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894250","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}