{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T03:21:04Z","timestamp":1729653664702,"version":"3.28.0"},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1109\/memcod.2016.7797743","type":"proceedings-article","created":{"date-parts":[[2016,12,29]],"date-time":"2016-12-29T21:54:22Z","timestamp":1483048462000},"page":"34-42","source":"Crossref","is-referenced-by-count":2,"title":["A computer-algebraic approach to formal verification of data-centric low-level software"],"prefix":"10.1109","author":[{"given":"Oliver","family":"Marx","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Villarraga","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","first-page":"547","article-title":"A lazy and layered SMT(BV) solver for hard industrial verification problems","author":"bruttomcsso","year":"0"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"ref12","first-page":"174","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"0"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2007.1073"},{"key":"ref14","first-page":"899","article-title":"Efficient Grobner 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":"ref15","first-page":"1","article-title":"Efficient symbolic computation for word-level abstraction from combinational circuits for verification over finite fields","volume":"pp","author":"pruss","year":"2015","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"first-page":"1","article-title":"Equivalence verification of large galois field arithmetic circuits using word-level abstraction via grobner bases","year":"0","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_45"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763035"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_6"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-005-0004-8"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker Blast: Applications to Software Engineering","volume":"9","author":"beyer","year":"2007","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjtsldm.6.135"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_20"},{"key":"ref8","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"},{"journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)","year":"2016","author":"barrett","key":"ref7"},{"key":"ref2","first-page":"168","article-title":"A tool for checking ansi c programs","author":"clarke","year":"2004","journal-title":"In Tools and Algorithms for the Construction and Analysis of Systems"},{"journal-title":"The Slam Project Debugging System Software via Static Analysis","year":"0","author":"ball","key":"ref1"},{"key":"ref9","article-title":"The yices SMT solver","author":"dutertre","year":"2006","journal-title":"SRI Computer Science Laboratory Technical Report"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"journal-title":"Renesas Electronics Corporation","article-title":"Sh-1\/sh-2\/sh-dsp software manual, rev. 5.0","year":"2005","key":"ref21"}],"event":{"name":"2016 ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)","start":{"date-parts":[[2016,11,18]]},"location":"Kanpur, India","end":{"date-parts":[[2016,11,20]]}},"container-title":["2016 ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7786794\/7797738\/07797743.pdf?arnumber=7797743","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T02:15:44Z","timestamp":1568686544000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7797743\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/memcod.2016.7797743","relation":{},"subject":[],"published":{"date-parts":[[2016,11]]}}}