{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:40Z","timestamp":1740134560997,"version":"3.37.3"},"reference-count":11,"publisher":"Wiley","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"name":"Chinese National 973 Plan","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}]},{"name":"Chinese National Key Technology R&D Program","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004147","name":"Tsinghua University","doi-asserted-by":"publisher","award":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"],"award-info":[{"award-number":["2010CB328003","SQ2012BAJY4052","61272001","60903030","91218302"]}],"id":[{"id":"10.13039\/501100004147","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>Satisfiability Modulo Theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based on DPLL(<jats:sans-serif>T<\/jats:sans-serif>), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(<jats:sans-serif>T<\/jats:sans-serif>)-based SMT solvers. The soundness and completeness for DPLL(<jats:sans-serif>T<\/jats:sans-serif>) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10%, which outperforms other methods, and the certificate checking procedure is quite time saving.<\/jats:p>","DOI":"10.1155\/2013\/964682","type":"journal-article","created":{"date-parts":[[2013,5,23]],"date-time":"2013-05-23T17:02:11Z","timestamp":1369328531000},"page":"1-13","source":"Crossref","is-referenced-by-count":0,"title":["A Unified Framework for DPLL(T) + Certificates"],"prefix":"10.1155","volume":"2013","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4679-0488","authenticated-orcid":true,"given":"Min","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9246-5"},{"key":"3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Z3: an efficient SMT solver","volume":"4963","year":"2008"},{"key":"6","series-title":"The Computational Complexity Column","first-page":"66","volume-title":"Propositional proof complexity: past, present, and future","year":"1998"},{"key":"8","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","year":"1962","journal-title":"Communications of the ACM"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"first-page":"333","volume-title":"An extensible SAT-solver","year":"2004","key":"11"},{"volume":"4, article 45","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation","year":"2008","key":"12"},{"issue":"1","key":"14","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"42","journal-title":"Formal Methods in System Design"},{"key":"16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants","volume":"3920","year":"2006"},{"key":"18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-540-72788-0_32","volume-title":"A simple and exible way of computing small unsatisfiable cores in SAT modulo theories","volume":"4501","year":"2007"},{"key":"21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Rocket-fast proof checking for SMT solvers","volume":"4963","year":"2008"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/964682.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/964682.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/964682.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T09:35:08Z","timestamp":1498037708000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2013\/964682\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":11,"alternative-id":["964682","964682"],"URL":"https:\/\/doi.org\/10.1155\/2013\/964682","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2013]]}}}