{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T00:10:35Z","timestamp":1771891835666,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642253782","type":"print"},{"value":"9783642253799","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_12","type":"book-chapter","created":{"date-parts":[[2011,11,13]],"date-time":"2011-11-13T20:33:47Z","timestamp":1321216427000},"page":"135-150","source":"Crossref","is-referenced-by-count":85,"title":["A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses"],"prefix":"10.1007","author":[{"given":"Michael","family":"Armand","sequence":"first","affiliation":[]},{"given":"Germain","family":"Faure","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Chantal","family":"Keller","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Source code of the development, http:\/\/www.lix.polytechnique.fr\/~keller\/Recherche\/smtcoq.html"},{"key":"12_CR2","unstructured":"SMT-LIB, http:\/\/www.smtlib.org"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann and Paulson [9], pp. 83\u201398","DOI":"10.1007\/978-3-642-14052-5_8"},{"issue":"3","key":"12_CR4","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. J. Autom. Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F. Besson","year":"2007","unstructured":"Besson, F.: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 48\u201362. Springer, Heidelberg (2007)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-Style Proof Reconstruction for Z3. In: Kaufmann and Paulson [9], pp. 179\u2013194","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"12_CR7","unstructured":"D\u00e9n\u00e8s, M.: Coq with native compilation, https:\/\/github.com\/maximedenes\/native-coq"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving","year":"2010","unstructured":"Kaufmann, M., Paulson, L.C. (eds.): ITP 2010. LNCS, vol.\u00a06172. Springer, Heidelberg (2010)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-04222-5_18","volume-title":"Frontiers of Combining Systems","author":"S. Lescuyer","year":"2009","unstructured":"Lescuyer, S., Conchon, S.: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 287\u2013303. Springer, Heidelberg (2009)"},{"issue":"2","key":"12_CR11","first-page":"43","volume":"144","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. ENTCS\u00a0144(2), 43\u201351 (2006)","journal-title":"ENTCS"},{"issue":"6","key":"12_CR12","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL. J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"12_CR13","unstructured":"Oe, D., Stump, A.: Extended Abstract: Combining a Logical Framework with an RUP Checker for SMT Proofs. In: Lahiri, S., Seshia, S. (eds.) Proceedings of the 9th International Workshop on Satisfiability Modulo Theories, Snowbird, USA (2011)"},{"key":"12_CR14","unstructured":"Tseitin, G.S.: On the complexity of proofs in propositional logics. Automation of Reasoning: Classical Papers in Computational Logic (1967-1970)\u00a02 (1983)"},{"key":"12_CR15","unstructured":"Weber, T.: SAT-based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany (April 2008), http:\/\/www.cl.cam.ac.uk\/~tw333\/publications\/weber08satbased.html"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T05:37:58Z","timestamp":1497937078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}