{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:26Z","timestamp":1725903386598},"publisher-location":"Cham","reference-count":32,"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"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_14","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"220-236","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":45,"title":["Efficient Certified RAT Verification"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"unstructured":"ACL2 Community. ACL2 documentation topic: FAST-ALISTS. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/current\/manual\/index.html?topic=ACL2____FAST-ALISTS","key":"14_CR1"},{"unstructured":"ACL2 Community. ACL2 documentation topic: STOBJ. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v7-2\/manual\/?topic=ACL2____STOBJ","key":"14_CR2"},{"unstructured":"ACL2 Community. ACL2 system and libraries on GitHub. https:\/\/github.com\/acl2\/acl2\/","key":"14_CR3"},{"unstructured":"ACL2 LRAT checker. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/sat\/lrat\/","key":"14_CR4"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivan\u010di\u0107","year":"2008","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science 404(3), 256\u2013274 (2008)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: Sat competition 2016: Recent developments. In: AAAI 2017 (2017)","key":"14_CR6","DOI":"10.1609\/aaai.v31i1.10641"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-40229-1_4","volume-title":"Automated Reasoning","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 (LNAI), vol. 9706, pp. 25\u201344. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_4"},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436\u2013453. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_43"},{"unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/","key":"14_CR10"},{"unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: $$KR\\tilde{O}$$ 1996, pp. 148\u2013159. Morgan Kaufmann (1996)","key":"14_CR11"},{"key":"14_CR12","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"},{"unstructured":"Cryptominisat v5. http:\/\/baldur.iti.kit.edu\/sat-competition-2016\/solvers\/main\/cmsat5_main2.zip","key":"14_CR13"},{"key":"14_CR14","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"},{"unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886\u201310891 (2003)","key":"14_CR15"},{"unstructured":"Heule, M.J.H.: The DRAT format and DRAT-trim checker. CoRR, abs\/1610.06229 (2016). Source code, https:\/\/github.com\/marijnheule\/drat-trim","key":"14_CR16"},{"unstructured":"Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All (APPA), July 2014. http:\/\/www.easychair.org\/smart-program\/VSL2014\/APPA-index.html","key":"14_CR17"},{"doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Trimming while checking clausal proofs. In: FMCAD, pp. 181\u2013188 (2013)","key":"14_CR18","DOI":"10.1109\/FMCAD.2013.6679408"},{"unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test., Verif. Reliab. 24(8), 593\u2013607 (2014)","key":"14_CR19"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction \u2013 CADE-25","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591\u2013606. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_40"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","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., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_15"},{"unstructured":"Kaufmann, M., Moore, J S.: An industrial strength theorem prover for a logic based on common LISP. IEEE Trans. Softw. Eng. 23(4), 203\u2013213 (1997)","key":"14_CR22"},{"doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: CADE-26. LNCS. Springer (to appear, 2017)","key":"14_CR23","DOI":"10.1007\/978-3-319-63046-5_15"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69407-6_39"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_14"},{"issue":"50","key":"14_CR26","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)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Maric, F., Janicic, P.: Formalization of abstract state transition systems for SAT. Logical Methods in Comput. Sci. 7(3) (2011)","key":"14_CR27","DOI":"10.2168\/LMCS-7(3:19)2011"},{"volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","year":"2002","author":"T Nipkow","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)","key":"14_CR28"},{"issue":"4","key":"14_CR29","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Producing and verifying extremely large propositional refutations - have your cake and eat it too. Ann. Math. Artif. Intell. 65(4), 329\u2013372 (2012)","journal-title":"Ann. Math. Artif. Intell."},{"key":"14_CR30","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":"ND Wetzler","year":"2013","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt Jr., 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":"14_CR31","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":"ND Wetzler","year":"2014","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt Jr., 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"},{"unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, pp. 10880\u201310885 (2003)","key":"14_CR32"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T18:03:58Z","timestamp":1659204238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"11 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gothenburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 August 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 August 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cade-26.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}
