{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:01:22Z","timestamp":1784844082463,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"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>(PR). 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 paper describes the first approach to formally verify PR proofs on a succinct representation; we present (i) a new<jats:italic>Linear PR<\/jats:italic>(LPR) proof format, (ii) a tool to efficiently convert PR proofs into LPR format, and (iii) , a verified LPR proof checker developed in CakeML. The LPR format is backwards compatible with the existing LRAT format, but extends the latter with support for the addition of PR 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 ones 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 and that the strong correctness guarantees are obtained without significant sacrifice in the performance of the verified executable.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_12","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"223-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["cake_lpr: Verified Propagation Redundancy Checking in CakeML"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.jlamp.2020.100530"},{"key":"12_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.\u00a07086, 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":"12_CR3","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":"12_CR4","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.\u00a01579, pp. 193\u2013207. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"12_CR5","doi-asserted-by":"crossref","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, Springer (2021), to appear","DOI":"10.26226\/morressier.604907f41a80aac83ca25ceb"},{"key":"12_CR6","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":"12_CR7","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"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Formally verifying the solution to the boolean Pythagorean triples problem. J. Autom. Reasoning 63(3), 695\u2013722 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9490-4","DOI":"10.1007\/s10817-018-9490-4"},{"key":"12_CR9","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":"12_CR10","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":"12_CR11","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":"12_CR12","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":"12_CR13","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":"12_CR14","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":"12_CR15","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":"12_CR16","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":"12_CR17","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":"12_CR18","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":"12_CR19","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":"12_CR20","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"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reasoning 64(3), 533\u2013554 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09516-0","DOI":"10.1007\/s10817-019-09516-0"},{"key":"12_CR22","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.\u00a09710, 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":"12_CR23","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":"12_CR24","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.\u00a07364, 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":"12_CR25","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":"12_CR26","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.artint.2015.03.004"},{"key":"12_CR27","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":"12_CR28","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reasoning 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","DOI":"10.1007\/s10817-019-09525-z"},{"key":"12_CR29","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":"12_CR30","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"12_CR31","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":"12_CR32","doi-asserted-by":"publisher","unstructured":"Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2-3), 284\u2013315(2014). https:\/\/doi.org\/10.1017\/S0956796813000282","DOI":"10.1017\/S0956796813000282"},{"key":"12_CR33","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.\u00a07148, 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":"12_CR34","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.\u00a05170, 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"},{"key":"12_CR35","doi-asserted-by":"publisher","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, \u00a0e2 (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","DOI":"10.1017\/S0956796818000229"},{"key":"12_CR36","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.\u00a08561, 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"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:43:47Z","timestamp":1671684227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}