{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:27Z","timestamp":1725903387361},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_15","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"237-254","source":"Crossref","is-referenced-by-count":21,"title":["Efficient Verified (UN)SAT Certificate Checking"],"prefix":"10.1007","author":[{"given":"Peter","family":"Lammich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"15_CR1","unstructured":"Back, R.-J.: On the correctness of refinement steps in program development. Ph.D. thesis, Department of Computer Science, University of Helsinki (1978)"},{"key":"15_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus - A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus - A Systematic Introduction. Springer, New York (1998)"},{"key":"15_CR3","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art the Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art the Calculus of Inductive Constructions, 1st edn. Springer, New York (2010)","edition":"1"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-40648-0_23","volume-title":"NASA Formal Methods","author":"J Brunner","year":"2016","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 307\u2013321. Springer, Cham (2016). doi: 10.1007\/978-3-319-40648-0_23"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","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., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71067-7_14"},{"key":"15_CR6","series-title":"Lecture Notes in Artificial Intelligence","first-page":"220","volume-title":"CADE 2017","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M., Hunt, W., Matt, K., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNAI, vol. 10395, pp. 220\u2013236. Springer, Cham (2017)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-662-54577-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_7"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260\u2013274. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14808-8_18"},{"key":"15_CR9","unstructured":"DRAT-TRIM GitHub repository. https:\/\/github.com\/marijnheule\/drat-trim"},{"key":"15_CR10","unstructured":"DRAT-TRIM homepage. https:\/\/www.cs.utexas.edu\/~marijn\/drat-trim\/"},{"key":"15_CR11","unstructured":"DRAT-TRIM issue tracker. https:\/\/github.com\/marijnheule\/drat-trim\/issues"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_31"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of DATE. IEEE (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction, pp. 169\u2013185. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0012"},{"key":"15_CR15","unstructured":"Haftmann, F.: Code generation from specifications in higher order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"F Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100\u2013115. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39634-2_10"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-12251-4_9"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M., Hunt, W., Wetzler, N.: Trimming while checking clausal proofs. In: 2013 Formal Methods in Computer-Aided Design, FMCAD 2013, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of POPL, pp. 179\u2013192. ACM (2014)","DOI":"10.1145\/2535838.2535841"},{"key":"15_CR20","unstructured":"Lammich, P.: Grat tool chain homepage. http:\/\/www21.in.tum.de\/lammich\/grat\/"},{"key":"15_CR21","unstructured":"Lammich, P.: Gratchk proof outline. http:\/\/www21.in.tum.de\/lammich\/grat\/outline.pdf"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","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, Heidelberg (2013). doi: 10.1007\/978-3-642-39634-2_9"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-08970-6_21","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2014","unstructured":"Lammich, P.: Verified efficient implementation of gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325\u2013340. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_21"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","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, Cham (2015). doi: 10.1007\/978-3-319-22102-1_17"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement based verification of imperative data structures. In: CPP, pp. 27\u201336. ACM (2016)","DOI":"10.1145\/2854065.2854067"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339\u2013354. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_24"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: CPP 2015, pp. 137\u2013146. ACM, New York (2015)","DOI":"10.1145\/2676724.2693165"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-43144-4_14","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2016","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 219\u2013234. Springer, Cham (2016). doi: 10.1007\/978-3-319-43144-4_14"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32347-8_12"},{"key":"15_CR30","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML","author":"R Milner","year":"1997","unstructured":"Milner, R., Harper, R., MacQueen, D., Tofte, M.: The Definition of Standard ML. MIT Press, Cambridge (1997)"},{"key":"15_CR31","unstructured":"MLton Standard ML compiler. http:\/\/mlton.org\/"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2\u20133","key":"15_CR33","doi-asserted-by":"crossref","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)","journal-title":"J. Funct. Program."},{"volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","key":"15_CR34","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"15_CR35","unstructured":"SAT competition (2013). http:\/\/satcompetition.org\/2013\/"},{"key":"15_CR36","unstructured":"SAT competition (2014). http:\/\/satcompetition.org\/2014\/"},{"key":"15_CR37","unstructured":"Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, vol. B-2016-1. University of Helsinki (2016)"},{"key":"15_CR38","unstructured":"SAT competition (2016). http:\/\/baldur.iti.kit.edu\/sat-competition-2016\/"},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006). doi: 10.1007\/11753728_60"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_24"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39634-2_18","volume-title":"Interactive Theorem Proving","author":"N Wetzler","year":"2013","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229\u2013244. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39634-2_18"},{"key":"15_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_31"},{"issue":"4","key":"15_CR43","doi-asserted-by":"crossref","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\u2013227 (1971)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T10:13:58Z","timestamp":1719310438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}