{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:32Z","timestamp":1771024232960,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319402284","type":"print"},{"value":"9783319402291","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_4","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"25-44","source":"Crossref","is-referenced-by-count":15,"title":["A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[]},{"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reasoning 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR2","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"issue":"2","key":"4_CR3","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"55","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reasoning 55(2), 155\u2013200 (2016)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"4_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-642-40885-4_17","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 245\u2013260. Springer, Heidelberg (2013)"},{"key":"4_CR7","unstructured":"Blanchette, J.C., Fleury, M., Schlichtkrull, A., Traytel, D.: IsaFoL: Isabelle formalization of logic. https:\/\/bitbucket.org\/jasmin_blanchette\/isafol"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/978-3-319-08587-6_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 46\u201360. Springer, Heidelberg (2014)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"issue":"2","key":"4_CR10","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"issue":"7","key":"4_CR11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"4_CR12","unstructured":"Fleury, M.: Formalisation of ground inference systems in a proof assistant. https:\/\/www.mpi-inf.mpg.de\/fileadmin\/inf\/rg1\/Documents\/fleury_master_thesis.pdf"},{"key":"4_CR13","unstructured":"Fleury, M., Blanchette, J.C.: Formalization of Weidenbach\u2019s Automated Reasoning\u2014The Art of Generic Problem Solving. https:\/\/bitbucket.org\/jasmin_blanchette\/isafol\/src\/master\/Weidenbach_Book\/README.md"},{"key":"4_CR14","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":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BFb0055135","volume-title":"Theorem Proving in Higher Order Logics","author":"JV Harrison","year":"1998","unstructured":"Harrison, J.V.: Formalizing basic first order model theory. In: Newey, M., Grundy, J. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 153\u2013170. Springer, Heidelberg (1998)"},{"issue":"8","key":"4_CR17","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1002\/stvr.1549","volume":"24","author":"MJ Heule","year":"2014","unstructured":"Heule, M.J., Hunt Jr., W.A., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. 24(8), 593\u2013607 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-61551-2_65","volume-title":"Principles and Practice of Constraint Programming - CP 1996","author":"RJ Bayardo Jr","year":"1996","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 46\u201360. Springer, Heidelberg (1996)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"4_CR20","volume-title":"The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability","author":"DE Knuth","year":"2015","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley, Reading (2015)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"4_CR22","unstructured":"Lescuyer, S.: Formalizing and implementing a reflexive tactic for automated deduction in Coq. Ph.D. thesis (2011)"},{"issue":"4","key":"4_CR23","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173\u2013180 (1993)","journal-title":"Inf. Process. Lett."},{"key":"4_CR24","unstructured":"Margetson, J., Ridge, T.: Completeness theorem, vol. 2004. Formal proof development. http:\/\/afp.sf.net\/entries\/Completeness.shtml"},{"key":"4_CR25","unstructured":"Mari\u0107, F.: Formal verification of modern SAT solvers. Archive of Formal Proofs (2008). Formal proof development. http:\/\/afp.sf.net\/entries\/SATSolverVerification.shtml"},{"issue":"50","key":"4_CR26","doi-asserted-by":"crossref","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theoret. Comput. Sci. 411(50), 4333\u20134356 (2010)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"4_CR27","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Math. Appl. 4(1), 3\u201324 (2005)","journal-title":"Mechanized Math. Appl."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"6","key":"4_CR29","doi-asserted-by":"crossref","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-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-27940-9_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Nipkow","year":"2012","unstructured":"Nipkow, T.: Teaching semantics with a proof assistant: no more LSD trip proofs. In: Rybalchenko, A., Kuncak, V. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 24\u201338. Springer, Heidelberg (2012)"},{"key":"4_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, New York (2014)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-642-27940-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Oe","year":"2012","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 363\u2013378. Springer, Heidelberg (2012)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol. 2, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Pierce, B.C.: Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009, pp. 121\u2013122. ACM (2009)","DOI":"10.1145\/1596550.1596552"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) FMCAD 2014, pp. 195\u2013202. IEEE Computer Society Press (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"4_CR37","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, Machines, and G\u00f6del\u2019s Proof","author":"N Shankar","year":"1994","unstructured":"Shankar, N.: Metamathematics, Machines, and G\u00f6del\u2019s Proof. Cambridge Tracts in Theoretical Computer Science, vol. 38. Cambridge University Press, Cambridge (1994)"},{"key":"4_CR38","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2011.03.002","volume":"269","author":"N Shankar","year":"2011","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. Electron. Notes Theoret. Comput. Sci. 269, 3\u201317 (2011)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP\u2014A new search algorithm for satisfiability. In: ICCAD 1996, pp. 220\u2013227. IEEE Computer Society Press (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"4_CR40","unstructured":"Sternagel, C., Thiemann, R.: An Isabelle\/HOL formalization of rewriting for certified termination analysis. http:\/\/cl-informatik.uibk.ac.at\/software\/ceta\/"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Heidelberg (2014)"},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-23506-6_12","volume-title":"Correct System Design","author":"C Weidenbach","year":"2015","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Olderog-Festschrift. LNCS, vol. 9360, pp. 172\u2013188. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-23506-6_12"},{"key":"4_CR43","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014A generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23). University of Bia\u0142ystok (2007)"},{"issue":"5","key":"4_CR44","first-page":"661","volume":"13","author":"J Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The verification grand challenge. J. Uni. Comput. Sci. 13(5), 661\u2013668 (2007)","journal-title":"J. Uni. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:28:49Z","timestamp":1748986129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}