{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T20:06:38Z","timestamp":1730232398335,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,11]]},"DOI":"10.1109\/iccad.2013.6691188","type":"proceedings-article","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T22:22:41Z","timestamp":1394230961000},"page":"677-684","source":"Crossref","is-referenced-by-count":0,"title":["Proof logging for computer algebra based SMT solving"],"prefix":"10.1109","author":[{"given":"Oliver","family":"Marx","sequence":"first","affiliation":[{"name":"Electronic Design Automation Group, TU Kaiserslautern"}]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[{"name":"Electronic Design Automation Group, TU Kaiserslautern"}]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[{"name":"Electronic Design Automation Group, TU Kaiserslautern"}]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[{"name":"Electronic Design Automation Group, TU Kaiserslautern"}]},{"given":"Alexander","family":"Dreyer","sequence":"additional","affiliation":[{"name":"Fraunhofer ITWM, Kaiserslautern"}]}],"member":"263","reference":[{"key":"19","first-page":"618","article-title":"A Gro?bner basis approach to CNF-formulae preprocessing","volume":"4424","author":"condrat","year":"2007","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"journal-title":"The RES File Format","year":"0","key":"17"},{"key":"18","article-title":"Verifying rup proofs of propositional unsatisfiability","author":"gelder","year":"2008","journal-title":"ISAIM"},{"key":"15","first-page":"75","article-title":"Picosat essentials","volume":"4","author":"biere","year":"2008","journal-title":"JSAT"},{"journal-title":"The RUP File Format","year":"0","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2011.6114160"},{"journal-title":"Singular 3-1-4 - A Computer Algebra System for Polynomial Computations","year":"2012","author":"decker","key":"14"},{"key":"11","first-page":"248","article-title":"Smtinterpol: An interpolating smt solver","author":"christ","year":"2012","journal-title":"SPIN"},{"key":"12","first-page":"899","article-title":"Efficient gro?bner basis reductions for formal verification of galois field multipliers","author":"lv","year":"2012","journal-title":"Design Automation Test in Europe Conference Exhibition (DATE) 2012"},{"key":"3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","article-title":"Efficient e-matching for SMT solvers","volume":"4603","author":"de moura","year":"2007","journal-title":"CADE Ser Lecture Notes in Computer Science"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"1","first-page":"81","article-title":"A fast linear-arithmetic solver for DPLL (T)","volume":"4144","author":"dutertre","year":"2006","journal-title":"Proc International Conference Computer Aided Verification (CAV) Ser LNCS"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.52"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.888277"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763035"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2007.1073"},{"key":"4","first-page":"174","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"2009","journal-title":"Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2009 Ser TACAS'09"},{"key":"9","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","author":"wienand","year":"2008","journal-title":"Proc International Conference Computer Aided Verification (CAV)"},{"key":"8","first-page":"22","article-title":"Modular-HED: A canonical decision diagram for modular equivalence verification of polynomial functions","author":"alizadeh","year":"2008","journal-title":"Workshop on Constraints in Formal Verification CFV Australia"}],"event":{"name":"2013 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)","start":{"date-parts":[[2013,11,18]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2013,11,21]]}},"container-title":["2013 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6679730\/6691081\/06691188.pdf?arnumber=6691188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T08:30:24Z","timestamp":1623141024000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/6691188\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/iccad.2013.6691188","relation":{},"subject":[],"published":{"date-parts":[[2013,11]]}}}