{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:40:54Z","timestamp":1768344054168,"version":"3.49.0"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1109\/fmcad.2016.7886666","type":"proceedings-article","created":{"date-parts":[[2017,3,28]],"date-time":"2017-03-28T02:52:44Z","timestamp":1490669564000},"page":"93-100","source":"Crossref","is-referenced-by-count":17,"title":["Lazy proofs for DPLL(T)-based SMT solvers"],"prefix":"10.1109","author":[{"given":"Guy","family":"Katz","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Liana","family":"Hadarean","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9152-7"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"ref13","article-title":"Extending SMTCoq, a Certified Checker for SMT","author":"ekici","year":"2016","journal-title":"HATT"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_11"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_24"},{"key":"ref16","article-title":"Proofs for Satisfiability Problems","author":"heule","year":"2015","journal-title":"All about Proofs Proofs for All"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_1"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref19","article-title":"Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite","author":"mclaughlin","year":"2005","journal-title":"PDPAR"},{"key":"ref4","author":"barrett","year":"0","journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)"},{"key":"ref3","article-title":"Proofs in Satisfiability Modulo Theories","author":"barrett","year":"2015","journal-title":"All about Proofs Proofs for All"},{"key":"ref6","article-title":"Proofs and Refutations, and Z3","author":"bjorner","year":"2008","journal-title":"LPAR"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_35"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"ref2","article-title":"CVC4","author":"barrett","year":"2011","journal-title":"CAV"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"ref1","article-title":"A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses","author":"armand","year":"2011","journal-title":"CPP"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_38"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref24","article-title":"SMT Proof Checking Using a Logical Framework","author":"stump","year":"2012","journal-title":"Formal Methods in System Design"},{"key":"ref23","article-title":"Certified Interpolant Generation for EUF","author":"reynolds","year":"2011","journal-title":"SMT"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-0349-4_5"}],"event":{"name":"2016 Formal Methods in Computer-Aided Design (FMCAD)","location":"Mountain View, CA, USA","start":{"date-parts":[[2016,10,3]]},"end":{"date-parts":[[2016,10,6]]}},"container-title":["2016 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7879555\/7886641\/07886666.pdf?arnumber=7886666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,13]],"date-time":"2017-12-13T20:55:29Z","timestamp":1513198529000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7886666\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2016.7886666","relation":{},"subject":[],"published":{"date-parts":[[2016,10]]}}}