{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:03:56Z","timestamp":1784844236821,"version":"3.55.0"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T00:00:00Z","timestamp":1677456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T00:00:00Z","timestamp":1677456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002835","name":"Chalmers University of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002835","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is <jats:italic>propagation redundancy<\/jats:italic> (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PR}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PR<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This article describes the first approach to formally verify <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PR}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PR<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> proofs on a succinct representation. We present (i) a new <jats:italic>Linear PR<\/jats:italic> (LPR) proof format, (ii) an extension of the  tool to efficiently convert <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PR}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PR<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> proofs into LPR format, and (iii) , a verified LPR proof checker developed in CakeML. We also enhance these tools with (iv) a new <jats:italic>compositional<\/jats:italic> proof format designed to enable separate (parallel) proof checking. The LPR format is backwards compatible with the existing LRAT format, but extends LRAT with support for the addition of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PR}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PR<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> clauses. Moreover,  is verified using CakeML \u2019s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing checkers because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that: LPR provides efficiency gains over existing proof formats;  \u2019s strong correctness guarantees are obtained without significant sacrifice in its performance; and the compositional proof format enables scalable parallel proof checking for large proofs.<\/jats:p>","DOI":"10.1007\/s10009-022-00690-y","type":"journal-article","created":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T14:03:01Z","timestamp":1677506581000},"page":"167-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML"],"prefix":"10.1007","volume":"25","author":[{"given":"Yong Kiam","family":"Tan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,2,27]]},"reference":[{"key":"690_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2020.100530","volume":"112","author":"O Abrahamsson","year":"2020","unstructured":"Abrahamsson, O.: A verified proof checker for higher-order logic. J. Log. Algebraic Methods Program. 112, 100530 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100530","journal-title":"J. Log. Algebraic Methods Program."},{"key":"690_CR2","doi-asserted-by":"publisher","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J., Shao, Z. (eds.) CPP, LNCS, vol. 7086, pp. 135\u2013150. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"690_CR3","doi-asserted-by":"publisher","unstructured":"Baek, S.: A formally verified checker for first-order proofs. In: Cohen, L., Kaliszyk, C. (eds.) ITP, LIPIcs, vol. 193, pp. 6:1\u20136:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.6","DOI":"10.4230\/LIPIcs.ITP.2021.6"},{"key":"690_CR4","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:3)2022","author":"S Baek","year":"2022","unstructured":"Baek, S., Carneiro, M., Heule, M.J.H.: A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci. (2022). https:\/\/doi.org\/10.46298\/lmcs-18(2:3)2022","journal-title":"Log. Methods Comput. Sci."},{"key":"690_CR5","doi-asserted-by":"publisher","unstructured":"Barnett, L.A., Biere, A.: Non-clausal redundancy properties. In: Platzer, A., Sutcliffe, G. (eds.) CADE, LNCS, vol. 12699, pp. 252\u2013272. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_15","DOI":"10.1007\/978-3-030-79876-5_15"},{"key":"690_CR6","doi-asserted-by":"publisher","unstructured":"Becker, H., Zyuzin, N., Monat, R., Darulova, E., Myreen, M.O., Fox, A.C.J.: A verified certificate checker for finite-precision error bounds in Coq and HOL4. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) FMCAD, pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603019","DOI":"10.23919\/FMCAD.2018.8603019"},{"key":"690_CR7","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) TACAS, LNCS, vol. 1579, pp. 193\u2013207. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"690_CR8","doi-asserted-by":"publisher","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: Groote, J.F., Larsen, K.G. (eds.) TACAS, LNCS, vol. 12651, pp. 76\u201393. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_5","DOI":"10.1007\/978-3-030-72016-2_5"},{"issue":"1\u20134","key":"690_CR9","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1\u20134), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5","journal-title":"J. Autom. Reason."},{"key":"690_CR10","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de\u00a0Moura, L. (ed.) CADE, LNCS, vol. 10395, pp. 220\u2013236. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"690_CR11","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS, LNCS, vol. 10205, pp. 118\u2013135 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7","DOI":"10.1007\/978-3-662-54577-5_7"},{"issue":"3","key":"690_CR12","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/s10817-018-9490-4","volume":"63","author":"L Cruz-Filipe","year":"2019","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Formally verifying the solution to the Boolean Pythagorean triples problem. J. Autom. Reason. 63(3), 695\u2013722 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9490-4","journal-title":"J. Autom. Reason."},{"key":"690_CR13","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT, LNCS, vol. 2919, pp. 502\u2013518. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"690_CR14","doi-asserted-by":"publisher","unstructured":"Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kuncak, V. (eds.) CAV, LNCS, vol. 10427, pp. 126\u2013133. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"690_CR15","doi-asserted-by":"publisher","unstructured":"F\u00e9r\u00e9e, H., Pohjola, J.\u00c5., Kumar, R., Owens, S., Myreen, M.O., Ho, S.: Program verification in the presence of I\/O - semantics, verified library routines, and verified applications. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE, LNCS, vol. 11294, pp. 88\u2013111. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_6","DOI":"10.1007\/978-3-030-03592-1_6"},{"key":"690_CR16","doi-asserted-by":"publisher","unstructured":"Fleury, M.: Optimizing a verified SAT solver. In: Badger, J.M., Rozier, K.Y. (eds.) NFM, LNCS, vol. 11460, pp. 148\u2013165. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_10","DOI":"10.1007\/978-3-030-20652-9_10"},{"key":"690_CR17","doi-asserted-by":"publisher","unstructured":"Fleury, M., Blanchette, J.C., Lammich, P.: A verified SAT solver with watched literals using Imperative HOL. In: Andronick, J., Felty, A.P. (eds.) CPP, pp. 158\u2013171. ACM (2018). https:\/\/doi.org\/10.1145\/3167080","DOI":"10.1145\/3167080"},{"key":"690_CR18","doi-asserted-by":"publisher","unstructured":"Ghale, M.K., Pattinson, D., Kumar, R., Norrish, M.: Verified certificate checking for counting votes. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE, LNCS, vol. 11294, pp. 69\u201387. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_5","DOI":"10.1007\/978-3-030-03592-1_5"},{"key":"690_CR19","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Yang, H. (ed.) ESOP, LNCS, vol. 10201, pp. 584\u2013610. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_22","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"690_CR20","doi-asserted-by":"publisher","unstructured":"Heule, M., Hunt Jr., W.A., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP, LNCS, vol. 10499, pp. 269\u2013284. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"690_CR21","doi-asserted-by":"publisher","unstructured":"Heule, M., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD, pp. 181\u2013188. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679408","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"690_CR22","doi-asserted-by":"publisher","unstructured":"Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC, LNCS, vol. 7261, pp. 50\u201365. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"690_CR23","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: McIlraith, S.A., Weinberger, K.Q. (eds.) AAAI, pp. 6598\u20136606. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"690_CR24","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Biere, A.: Compositional propositional proofs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR, LNCS, vol. 9450, pp. 444\u2013459. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_31","DOI":"10.1007\/978-3-662-48899-7_31"},{"key":"690_CR25","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M. (eds.) TACAS, LNCS, vol. 10806, pp. 75\u201392. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_5","DOI":"10.1007\/978-3-319-89963-3_5"},{"key":"690_CR26","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Clausal proofs of mutilated chessboards. In: Badger, J.M., Rozier, K.Y. (eds.) NFM, LNCS, vol. 11460, pp. 204\u2013210. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_13","DOI":"10.1007\/978-3-030-20652-9_13"},{"key":"690_CR27","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Vojnar, T., Zhang, L. (eds.) TACAS, LNCS, vol. 11427, pp. 41\u201358. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_3","DOI":"10.1007\/978-3-030-17462-0_3"},{"issue":"3","key":"690_CR28","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/s10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reason. 64(3), 533\u2013554 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09516-0","journal-title":"J. Autom. Reason."},{"key":"690_CR29","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Berre, D.L., (eds.) SAT, LNCS, vol. 9710, pp. 228\u2013245. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"690_CR30","doi-asserted-by":"publisher","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the Alloy constraint analyzer. In: Ghezzi, C., Jazayeri, M., Wolf, A.L. (eds.) ICSE, pp. 730\u2013733. ACM (2000). https:\/\/doi.org\/10.1145\/337180.337616","DOI":"10.1145\/337180.337616"},{"key":"690_CR31","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR, LNCS, vol. 7364, pp. 355\u2013370. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"690_CR32","unstructured":"Kanabar, H.: Implementing and verifying a compiler optimisation for CakeML (2018). https:\/\/hrutvik.co.uk\/assets\/pdf\/Hrutvik_Kanabar_dissertation.pdf. Computer Science Tripos, Part II Dissertation. University of Cambridge, UK"},{"key":"690_CR33","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Fleury, M., Biere, A.: The proof checkers Pacheck and Past\u00e8que for the practical algebraic calculus. In: FMCAD, pp. 264\u2013269. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_34","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_34"},{"key":"690_CR34","doi-asserted-by":"publisher","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR, LNCS, vol. 10900, pp. 516\u2013531. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_34","DOI":"10.1007\/978-3-319-94205-6_34"},{"key":"690_CR35","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.03.004","journal-title":"Artif. Intell."},{"key":"690_CR36","doi-asserted-by":"publisher","unstructured":"Kumar, R., Mullen, E., Tatlock, Z., Myreen, M.O.: Software verification with ITPs should use binary code extraction to reduce the TCB - (short paper). In: Avigad, J., Mahboubi, A. (eds.) ITP, LNCS, vol. 10895, pp. 362\u2013369. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_21","DOI":"10.1007\/978-3-319-94821-8_21"},{"key":"690_CR37","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) ITP, LIPIcs, vol. 141, pp. 22:1\u201322:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"issue":"4","key":"690_CR38","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to Imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9437-1","journal-title":"J. Autom. Reason."},{"issue":"3","key":"690_CR39","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"issue":"7","key":"690_CR40","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"690_CR41","unstructured":"Lind, J., Mihajlovic, N., Myreen, M.O.: Verified hash map and buffered I\/O libraries for CakeML. In: Trends in Functional Programming (TFP) (2021). Accepted for presentation"},{"key":"690_CR42","doi-asserted-by":"publisher","unstructured":"L\u00f6\u00f6w, A., Kumar, R., Tan, Y.K., Myreen, M.O., Norrish, M., Abrahamsson, O., Fox, A.C.J.: Verified compilation on a verified processor. In: McKinley, K.S., Fisher, K. (eds.) PLDI, pp. 1041\u20131053. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314622","DOI":"10.1145\/3314221.3314622"},{"issue":"50","key":"690_CR43","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Maric","year":"2010","unstructured":"Maric, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.09.014","journal-title":"Theor. Comput. Sci."},{"key":"690_CR44","doi-asserted-by":"publisher","unstructured":"Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: \u0152uf: minimizing the Coq extraction TCB. In: Andronick, J., Felty, A.P. (eds.) CPP, pp. 172\u2013185. ACM (2018). https:\/\/doi.org\/10.1145\/3167089","DOI":"10.1145\/3167089"},{"key":"690_CR45","doi-asserted-by":"publisher","unstructured":"Myreen, M.O.: The CakeML project\u2019s quest for ever stronger correctness theorems (invited paper). In: Cohen, L., Kaliszyk, C. (eds.) ITP, LIPIcs, vol. 193, pp. 1:1\u20131:10. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.1","DOI":"10.4230\/LIPIcs.ITP.2021.1"},{"issue":"2\u20133","key":"690_CR46","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1017\/S0956796813000282","volume":"24","author":"MO Myreen","year":"2014","unstructured":"Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2\u20133), 284\u2013315 (2014). https:\/\/doi.org\/10.1017\/S0956796813000282","journal-title":"J. Funct. Program."},{"key":"690_CR47","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Ro\u00dfkopf, S.: Isabelle\u2019s metalogic: Formalization and proof checker. In: Platzer, A., Sutcliffe, G. (eds.) CADE, LNCS, vol. 12699, pp. 93\u2013110. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_6","DOI":"10.1007\/978-3-030-79876-5_6"},{"key":"690_CR48","doi-asserted-by":"publisher","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: A verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI, LNCS, vol. 7148, pp. 363\u2013378. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_24","DOI":"10.1007\/978-3-642-27940-9_24"},{"key":"690_CR49","doi-asserted-by":"publisher","unstructured":"Reeves, J.E., Heule, M.J.H., Bryant, R.E.: Preprocessing of propagation redundant clauses. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR, LNCS, vol. 13385, pp. 106\u2013124. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_8","DOI":"10.1007\/978-3-031-10769-6_8"},{"key":"690_CR50","unstructured":"Slind, K.: Trusted extensions of interactive theorem provers: Workshop summary (2010). https:\/\/www.cs.utexas.edu\/users\/kaufmann\/itp-trusted-extensions-aug-2010\/summary\/summary.pdf. [Online; accessed 7-September-2021]"},{"key":"690_CR51","doi-asserted-by":"publisher","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, LNCS, vol. 5170, pp. 28\u201332. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6","DOI":"10.1007\/978-3-540-71067-7_6"},{"issue":"POPL","key":"690_CR52","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/3371076","volume":"4","author":"M Sozeau","year":"2020","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! Verification of type checking and erasure for Coq. Coq. Proc. ACM Program. Lang. 4(POPL), 8:1-8:28 (2020). https:\/\/doi.org\/10.1145\/3371076","journal-title":"Coq. Proc. ACM Program. Lang."},{"key":"690_CR53","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: Verified propagation redundancy checking in CakeML. In: Groote, J.F., Larsen, K.G. (eds.) TACAS, LNCS, vol. 12652, pp. 223\u2013241. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_12","DOI":"10.1007\/978-3-030-72013-1_12"},{"key":"690_CR54","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229","volume":"29","author":"YK Tan","year":"2019","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A.C.J., Owens, S., Norrish, M.: The verified CakeML compiler backend. J. Funct. Program. 29, e2 (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","journal-title":"J. Funct. Program."},{"key":"690_CR55","doi-asserted-by":"publisher","unstructured":"Wetzler, N., Heule, M., Hunt Jr., W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT, LNCS, vol. 8561, pp. 422\u2013429. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"690_CR56","doi-asserted-by":"publisher","unstructured":"Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: A framework for parallelized bounded model checking. In: Brim, L., van\u00a0de Pol, J. (eds.) PDMC, EPTCS, vol.\u00a014, pp. 62\u201376 (2009). https:\/\/doi.org\/10.4204\/EPTCS.14.5","DOI":"10.4204\/EPTCS.14.5"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00690-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00690-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00690-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T15:24:08Z","timestamp":1679930648000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00690-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,27]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["690"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00690-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,2,27]]},"assertion":[{"value":"4 November 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 February 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}