{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:53:04Z","timestamp":1777636384726,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_14","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"179-194","source":"Crossref","is-referenced-by-count":66,"title":["Fast LCF-Style Proof Reconstruction for Z3"],"prefix":"10.1007","author":[{"given":"Sascha","family":"B\u00f6hme","sequence":"first","affiliation":[]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"14_CR2","series-title":"Real-Time Safety Critical Systems Series","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/B978-0-444-89901-9.50012-4","volume-title":"The HOL logic and system. In: Towards Verified Systems","author":"M.J.C. Gordon","year":"1994","unstructured":"Gordon, M.J.C., Pitts, A.M.: The HOL logic and system. In: Towards Verified Systems. Real-Time Safety Critical Systems Series, vol.\u00a02, pp. 49\u201370. Elsevier, Amsterdam (1994)"},{"key":"14_CR3","volume-title":"Decision Procedures\u00a0\u2013 An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures\u00a0\u2013 An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"14_CR4","unstructured":"Collavizza, H., Gordon, M.: Integration of theorem-proving and constraint programming for software verification. Technical report, Laboratoire d\u2019Informatique, Signaux et Syst\u00e8mes de Sophia-Antipolis (2008)"},{"issue":"1-2","key":"14_CR5","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/s10817-009-9142-9","volume":"44","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie \u2014 An Interactive Prover-Backend for the Verifying C Compiler. J. Automated Reasoning\u00a044(1-2), 111\u2013144 (2010)","journal-title":"J. Automated Reasoning"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: 7th International Workshop on Satisfiability Modulo Theories, SMT \u201909 (2009)","DOI":"10.1145\/1670412.1670413"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"14_CR9","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings. vol.\u00a0418, CEUR-WS.org (2008)"},{"key":"14_CR10","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2 (August 2006), \n                    \n                      http:\/\/combination.cs.uiowa.edu\/smtlib\/papers\/format-v1.2-r06.08.30.pdf\n                    \n                    \n                   (retrieved January 21, 2010)"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","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. Electronic Notes in Theoretical Computer Science\u00a0144(2), 43\u201351 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"14_CR12","unstructured":"Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: A preliminary report. In: 6th International Workshop on Satisfiability Modulo Theories, SMT \u201908 (2008)"},{"key":"14_CR13","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.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"14_CR14","unstructured":"Hurlin, C., Chaieb, A., Fontaine, P., Merz, S., Weber, T.: Practical proof reconstruction for first-order logic and set-theoretical constructions. In: Proceedings of the Isabelle Workshop 2007, Bremen, Germany, July 2007, pp. 2\u201313 (2007)"},{"key":"14_CR15","unstructured":"B\u00f6hme, S.: Proof reconstruction for Z3 in Isabelle\/HOL. In: 7th International Workshop on Satisfiability Modulo Theories, SMT \u201909 (2009)"},{"issue":"1","key":"14_CR16","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic\u00a07(1), 26\u201340 (2009)","journal-title":"J. Applied Logic"},{"key":"#cr-split#-14_CR17.1","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA ???03), pp. 56???68 (2003);"},{"key":"#cr-split#-14_CR17.2","unstructured":"Number NASA\/CP-2003-212448 in NASA Technical Reports"},{"key":"14_CR18","unstructured":"Hurd, J.: Metis performance benchmarks, \n                    \n                      http:\/\/www.gilith.com\/software\/metis\/performance.html\n                    \n                    \n                   (retrieved January\u00a021, 2010)"},{"key":"14_CR19","unstructured":"HOL88 contributors: HOL88 source code, \n                    \n                      http:\/\/www.ftp.cl.cam.ac.uk\/ftp\/hvg\/hol88\/holsys.tar.gz\n                    \n                    \n                   (retrieved January\u00a021, 2010)"},{"key":"14_CR20","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: 5th Annual Satisfiability Modulo Theories Competition. In: SMT-COMP \u201909 (2009), \n                    \n                      http:\/\/www.smtcomp.org\/2009\/"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/10930755_5","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Norrish","year":"2003","unstructured":"Norrish, M.: Complete integer decision procedures as derived rules in HOL. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 71\u201386. Springer, Heidelberg (2003)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"14_CR23","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (2009)"},{"issue":"3-4","key":"14_CR24","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s10817-008-9109-2","volume":"41","author":"H. Amjad","year":"2008","unstructured":"Amjad, H.: Data compression for proof replay. J. Automated Reasoning\u00a041(3-4), 193\u2013218 (2008)","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:19Z","timestamp":1619785039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}