{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T21:12:41Z","timestamp":1725657161150},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987606","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"139-146","source":"Crossref","is-referenced-by-count":15,"title":["Leveraging linear and mixed integer programming for SMT"],"prefix":"10.1109","author":[{"given":"Tim","family":"King","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"journal-title":"GNU Linear Programming Kit","year":"0","author":"makhorin","key":"17"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.07.009"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1287\/opre.49.3.363.11211"},{"key":"16","first-page":"171","article-title":"Cvc4","author":"barrett","year":"2011","journal-title":"CAV"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-013-0055-6"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0433-3"},{"key":"11","first-page":"150","article-title":"The opensmt solver","author":"bruttomesso","year":"2011","journal-title":"TACAS"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2006.12.010"},{"key":"21","first-page":"337","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"TACAS"},{"key":"20","article-title":"The math-sat5 smt solver","author":"cimatti","year":"2013","journal-title":"TACAS"},{"key":"22","first-page":"737","article-title":"Yices 2.2","author":"dutertre","year":"2014","journal-title":"CAV"},{"journal-title":"The Alt-Ergo Automated Theorem Prover","year":"0","author":"bobot","key":"23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_8"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_26"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-008-0001-1"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679409"},{"key":"2","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability IOS"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_42"},{"key":"1","first-page":"81","article-title":"A fast linear-Arithmetic solver for dpll(t","author":"dutertre","year":"2006","journal-title":"CAV"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_8"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_17"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1002\/9781118627372"},{"journal-title":"Integrating Simplex with DPLL(T)","year":"2006","author":"dutertre","key":"4"},{"key":"9","article-title":"Experiments on the feasibility of using a floating-point simplex in an smt solver","author":"de oliveira","year":"2012","journal-title":"PAAR CEUR"},{"key":"8","first-page":"294","article-title":"The barcelogic smt solver","author":"bofill","year":"2008","journal-title":"CAV"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2014,10,21]]},"location":"Lausanne, Switzerland","end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987606.pdf?arnumber=6987606","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:08:50Z","timestamp":1490314130000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987606\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987606","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}