{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T20:39:22Z","timestamp":1648845562071},"reference-count":17,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T00:00:00Z","timestamp":1120176000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":2950,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2005,7]]},"DOI":"10.1016\/j.entcs.2004.06.067","type":"journal-article","created":{"date-parts":[[2005,7,7]],"date-time":"2005-07-07T15:24:27Z","timestamp":1120749867000},"page":"53-68","source":"Crossref","is-referenced-by-count":0,"title":["Validated Proof-Producing Decision Procedures"],"prefix":"10.1016","volume":"125","author":[{"given":"Robert","family":"Klapper","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/j.entcs.2004.06.067_bib001","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0956796803004921","article-title":"Dependent Types Ensure Partial Correctness of Theorem Provers","volume":"14","author":"Appel","year":"2002","journal-title":"Journal of Functional Programming"},{"issue":"3\u20134","key":"10.1016\/j.entcs.2004.06.067_bib002","article-title":"A Trustworthy Proof Checker","volume":"31","author":"Appel","year":"2003","journal-title":"Journal of Automated Reasoning, special issue on Proof-Carrying Code"},{"key":"10.1016\/j.entcs.2004.06.067_bib003","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In 14th International Conference on Computer-Aided Verification, 2002","DOI":"10.1007\/3-540-45657-0_18"},{"key":"10.1016\/j.entcs.2004.06.067_bib004","series-title":"Pragmatics of Decision Procedures in Automated Reasoning","article-title":"Combining SAT Methods with Non-Clausal Decision Heuristics","author":"Barrett","year":"2004"},{"key":"10.1016\/j.entcs.2004.06.067_bib005","first-page":"363","article-title":"The Rewriting Calculus - Part I","volume":"9","author":"Cirstea","year":"2001","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"10.1016\/j.entcs.2004.06.067_bib006","series-title":"Introduction to Algorithms","author":"Cormen","year":"1992"},{"key":"10.1016\/j.entcs.2004.06.067_bib007","doi-asserted-by":"crossref","unstructured":"E. Deplagne, C. Kirchner, H. Kirchner, and Q. Nguyen. Proof Search and Proof Check for Equational and Inductive Theorems. In F. Baader, editor, Conference on Automated Deduction - CADE-19, Miami, USA, 2003","DOI":"10.1007\/978-3-540-45085-6_26"},{"issue":"4","key":"10.1016\/j.entcs.2004.06.067_bib008","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","article-title":"Variations on the Common Subexpression Problem","volume":"27","author":"Downey","year":"1980","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"1","key":"10.1016\/j.entcs.2004.06.067_bib009","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A Framework for Defining Logics","volume":"40","author":"Harper","year":"1993","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"2","key":"10.1016\/j.entcs.2004.06.067_bib010","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","article-title":"Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors","volume":"35","author":"Velev","year":"2003","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/j.entcs.2004.06.067_bib011","doi-asserted-by":"crossref","unstructured":"G. Necula. Proof-Carrying Code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106\u2013119, January 1997","DOI":"10.1145\/263699.263712"},{"key":"10.1016\/j.entcs.2004.06.067_bib012","doi-asserted-by":"crossref","unstructured":"G. Necula and P. Lee. Proof Generation in the Touchstone Theorem Prover. In David McAllester, editor, 17th International Conference on Automated Deduction, 2000","DOI":"10.1007\/10721959_3"},{"key":"10.1016\/j.entcs.2004.06.067_bib013","unstructured":"A. Stump. Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University, 2002. available from http:\/\/www.cse.wustl.edu\/~stump\/"},{"key":"10.1016\/j.entcs.2004.06.067_bib014","unstructured":"A. Stump. Imperative LF Meta-Programming. In C. Sch\u00fcrmann, editor, Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004"},{"key":"10.1016\/j.entcs.2004.06.067_bib015","doi-asserted-by":"crossref","unstructured":"A. Stump, R. Besand, J. Brodman, J. Hseu, and B. Kinnersley. From Rogue to MicroRogue. In International Workshop on Rewriting Logic and Applications, 2004","DOI":"10.1016\/j.entcs.2004.06.028"},{"key":"10.1016\/j.entcs.2004.06.067_bib016","unstructured":"A. Stump, A. Deivanayagam, S. Kathol, D. Lingelbach, and D. Schobel. Rogue Decision Procedures. In C. Tinelli and S. Ranise, editors, 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2003"},{"key":"10.1016\/j.entcs.2004.06.067_bib017","series-title":"Basic Proof Theory","author":"Troelstra","year":"2000"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105050723?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105050723?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T05:23:40Z","timestamp":1586323420000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105050723"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["S1571066105050723"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2004.06.067","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,7]]}}}