{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:48Z","timestamp":1775868528953,"version":"3.50.1"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,3,12]],"date-time":"2018-03-12T00:00:00Z","timestamp":1520812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9455-7","type":"journal-article","created":{"date-parts":[[2018,3,12]],"date-time":"2018-03-12T15:59:51Z","timestamp":1520870391000},"page":"333-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality"],"prefix":"10.1007","volume":"61","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,12]]},"reference":[{"key":"9455_CR1","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"9455_CR2","doi-asserted-by":"publisher","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. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"key":"9455_CR3","series-title":"LNCS","first-page":"46","volume-title":"CP96","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.) CP96. LNCS, vol. 1118, pp. 46\u201360. Springer, Berlin (1996)"},{"key":"9455_CR4","unstructured":"Becker, H., Blanchette, J.C., Fleury, M., From, A.H., Jensen, A.B., Lammich, P., Larsen, J.B., Michaelis, J., Nipkow, T., Popescu, A., Schlichtkrull, A., Tourret, S., Traytel, D., Villadsen, J.: IsaFoL: Isabelle Formalization of Logic. https:\/\/bitbucket.org\/isafol\/isafol\/ . Accessed 13 Feb 2018"},{"key":"9455_CR5","series-title":"LNCS","first-page":"237","volume-title":"SAT 2015","author":"A Biere","year":"2015","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 5584, pp. 237\u2013243. Springer, Berlin (2015)"},{"key":"9455_CR6","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"9455_CR7","doi-asserted-by":"publisher","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. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"9455_CR8","series-title":"LNCS","first-page":"12","volume-title":"FroCoS 2011","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, Berlin (2011)"},{"key":"9455_CR9","series-title":"LNCS","first-page":"245","volume-title":"FroCoS 2013","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, Berlin (2013)"},{"issue":"2","key":"9455_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","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. Reason. 56(2), 155\u2013200 (2016)","journal-title":"J. Autom. Reason."},{"key":"9455_CR11","series-title":"LNCS","first-page":"25","volume-title":"IJCAR 2016","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 25\u201344. Springer, Berlin (2016)"},{"issue":"1","key":"9455_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017)","journal-title":"J. Autom. Reason."},{"key":"9455_CR13","series-title":"LNCS","first-page":"179","volume-title":"ITP 2010","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, Berlin (2010)"},{"key":"9455_CR14","series-title":"LNCS","first-page":"134","volume-title":"TPHOLs 2008","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Berlin (2008)"},{"issue":"2","key":"9455_CR15","doi-asserted-by":"publisher","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. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9455_CR16","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 220\u2013236. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"issue":"7","key":"9455_CR17","doi-asserted-by":"publisher","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":"9455_CR18","series-title":"LNCS","first-page":"502","volume-title":"SAT 2003","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Berlin (2003)"},{"key":"9455_CR19","unstructured":"Fleury, M.: Formalisation of Ground Inference Systems in a Proof Assistant. M.Sc. thesis, \u00c9cole normale sup\u00e9rieure de Rennes (2015). https:\/\/www.mpi-inf.mpg.de\/fileadmin\/inf\/rg1\/Documents\/fleury_master_thesis.pdf . Accessed 13 Feb 2018"},{"key":"9455_CR20","unstructured":"Fleury, M., Blanchette, J.C.: Formalization of Weidenbach\u2019s Automated Reasoning\u2014The Art of Generic Problem Solving (2017). https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/Weidenbach_Book\/README.md , Formal proof development. Accessed 13 Feb 2018"},{"key":"9455_CR21","unstructured":"Goel, A., Grundy, J.: Decision Procedure Toolkit. http:\/\/dpt.sourceforge.net\/ . Accessed 13 Feb 2018"},{"key":"9455_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation, LNCS","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, Berlin (1979)"},{"key":"9455_CR23","series-title":"LNCS","first-page":"103","volume-title":"FLOPS 2010","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, Berlin (2010)"},{"key":"9455_CR24","series-title":"LNCS","first-page":"153","volume-title":"TPHOLs \u201998","author":"J Harrison","year":"1998","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs \u201998. LNCS, vol. 1479, pp. 153\u2013170. Springer, Berlin (1998)"},{"key":"9455_CR25","series-title":"LNCS","first-page":"149","volume-title":"TPHOLs \u201999","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 \u201999. LNCS, vol. 1690, pp. 149\u2013166. Springer, Berlin (1999)"},{"key":"9455_CR26","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol. 4, Fascicle 6: Satisfiability. Addison-Wesley, Boston (2015)"},{"key":"9455_CR27","series-title":"LNCS","first-page":"589","volume-title":"IJCAR 2006","author":"A Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 589\u2013603. Springer, Berlin (2006)"},{"key":"9455_CR28","series-title":"LNCS","first-page":"1","volume-title":"FroCoS 2007","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS, vol. 4720, pp. 1\u201327. Springer, Berlin (2007)"},{"key":"9455_CR29","unstructured":"Lammich, P.: The Imperative Refinement Framework. Archive of Formal Proofs 2016. http:\/\/isa-afp.org\/entries\/Refine_Imperative_HOL.shtml , Formal proof development. Accessed 13 Feb 2018"},{"key":"9455_CR30","series-title":"LNCS","first-page":"84","volume-title":"ITP 2013","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84\u201399. Springer, Berlin (2013)"},{"key":"9455_CR31","series-title":"LNCS","first-page":"253","volume-title":"ITP 2015","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Berlin (2015)"},{"key":"9455_CR32","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/2854065.2854067","volume-title":"CPP 2016","author":"P Lammich","year":"2016","unstructured":"Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 27\u201336. ACM, New York (2016)"},{"key":"9455_CR33","series-title":"LNCS","first-page":"237","volume-title":"CADE-26","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 237\u2013254. Springer, Berlin (2017)"},{"key":"9455_CR34","unstructured":"Lescuyer, S.: Formalizing and implementing a reflexive tactic for automated deduction in Coq. Ph.D. thesis, Universit\u00e9 Paris-Sud (2011)"},{"issue":"4","key":"9455_CR35","doi-asserted-by":"publisher","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":"9455_CR36","unstructured":"Margetson, J., Ridge, T.: Completeness theorem. Archive of Formal Proofs 2004. http:\/\/isa-afp.org\/entries\/Completeness.shtml , Formal proof development. Accessed 13 Feb 2018"},{"key":"9455_CR37","unstructured":"Mari\u0107, F.: Formal verification of modern SAT solvers. Archive of Formal Proofs 2008. http:\/\/isa-afp.org\/entries\/SATSolverVerification.shtml , Formal proof development. Accessed 13 Feb 2018"},{"issue":"50","key":"9455_CR38","doi-asserted-by":"publisher","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. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"9455_CR39","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F., Jani\u010di\u0107, P.: Formalization of abstract state transition systems for SAT. Log. Methods Comput. Sci. 7(3) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:19)2011","DOI":"10.2168\/LMCS-7(3:19)2011"},{"key":"9455_CR40","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP\u2013a new search algorithm for satisfiability. In: ICCAD \u201996, pp. 220\u2013227. IEEE Computer Society Press, Silver Spring (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"issue":"1","key":"9455_CR41","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4(1), 3\u201324 (2005)","journal-title":"Mech. Math. Appl."},{"key":"9455_CR42","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, New York (2001)","DOI":"10.1145\/378239.379017"},{"issue":"6","key":"9455_CR43","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(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9455_CR44","series-title":"LNCS","first-page":"24","volume-title":"VMCAI 2012","author":"T Nipkow","year":"2012","unstructured":"Nipkow, T.: Teaching semantics with a proof assistant: no more LSD trip proofs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 24\u201338. Springer, Berlin (2012)"},{"key":"9455_CR45","doi-asserted-by":"publisher","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, Berlin (2014)"},{"key":"9455_CR46","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS","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, Berlin (2002)"},{"key":"9455_CR47","first-page":"363","volume-title":"VMCAI 2012, LNCS","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, Berlin (2012)"},{"key":"9455_CR48","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol.\u00a02, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"9455_CR49","first-page":"121","volume-title":"ICFP 2009","author":"BC Pierce","year":"2009","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, New York (2009)"},{"key":"9455_CR50","first-page":"195","volume-title":"FMCAD 2014","author":"A Reynolds","year":"2014","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, Silver Spring (2014)"},{"key":"9455_CR51","series-title":"LNCS","first-page":"341","volume-title":"ITP 2016","author":"A Schlichtkrull","year":"2016","unstructured":"Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 341\u2013357. Springer, Berlin (2016)"},{"key":"9455_CR52","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, Machines, and G\u00f6del\u2019s Proof, Cambridge Tracts in Theoretical Computer Science","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":"9455_CR53","doi-asserted-by":"publisher","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. Electr. Notes Theor. Comput. Sci. 269, 3\u201317 (2011)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9455_CR54","series-title":"LNCS","first-page":"237","volume-title":"SAT 2009","author":"N S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 9340, pp. 237\u2013243. Springer, Berlin (2009)"},{"key":"9455_CR55","unstructured":"Sternagel, C., Thiemann, R.: An Isabelle\/HOL formalization of rewriting for certified termination analysis. http:\/\/cl-informatik.uibk.ac.at\/software\/ceta\/ . Accessed 13 Feb 2018"},{"key":"9455_CR56","series-title":"LNCS","first-page":"696","volume-title":"CAV 2014","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, Berlin (2014)"},{"key":"9455_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-23506-6_12","volume-title":"Correct System Design: Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday","author":"C Weidenbach","year":"2015","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design: Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday. LNCS, vol. 9360, pp. 172\u2013188. Springer, Berlin (2015)"},{"key":"9455_CR58","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":"4","key":"9455_CR59","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221 (1971)","journal-title":"Commun. ACM"},{"issue":"5","key":"9455_CR60","first-page":"661","volume":"13","author":"J Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The verification grand challenge. J. Univers. Comput. Sci. 13(5), 661\u2013668 (2007)","journal-title":"J. Univers. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9455-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9455-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9455-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T18:42:53Z","timestamp":1751481773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9455-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,12]]},"references-count":60,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9455"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9455-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,12]]},"assertion":[{"value":"31 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}