{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:29Z","timestamp":1748413529149},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642148071"},{"type":"electronic","value":"9783642148088"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14808-8_18","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T09:52:01Z","timestamp":1282384321000},"page":"260-274","source":"Crossref","is-referenced-by-count":20,"title":["Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking"],"prefix":"10.1007","author":[{"given":"Ashish","family":"Darbari","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Fischer","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-57826-9_127","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"C.M. Angelo","year":"1994","unstructured":"Angelo, C.M., Claesen, L., De Man, H.: Degrees of formality in shallow embedding hardware description languages in HOL. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 89\u2013100. Springer, Heidelberg (1994)"},{"key":"18_CR2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res.\u00a022, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions (2004)","key":"18_CR3","DOI":"10.1007\/978-3-662-07964-5"},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. J. Satisfiability, Boolean Modeling and Computation\u00a04, 75\u201397 (2008)","journal-title":"J. Satisfiability, Boolean Modeling and Computation"},{"key":"18_CR5","volume-title":"Advances in Computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. In: Advances in Computers. Academic Press, London (2003)"},{"key":"18_CR6","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.\u00a05170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Inf. Comput.\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG 1988","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"18_CR10","first-page":"10886","volume-title":"Proc. Design, Automation and Test in Europe","author":"E.I. Goldberg","year":"2003","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proc. Design, Automation and Test in Europe, pp. 10886\u201310891. IEEE, Los Alamitos (2003)"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/s10009-004-0152-y","volume":"7","author":"J. Hammarberg","year":"2005","unstructured":"Hammarberg, J., Nadjm-Tehrani, S.: Formal verification of fault tolerance in safety-critical reconfigurable modules. J. Software Tools for Technology Transfer\u00a07(3), 268\u2013279 (2005)","journal-title":"J. Software Tools for Technology Transfer"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X. Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal Verification of a C-like Memory Model and its uses for Verifying Program Transformations. J. Automated Reasoning\u00a041(1), 1\u201331 (2008)","journal-title":"J. Automated Reasoning"},{"unstructured":"Lescuyer, S., Conchon, S.: A reflexive formalization of a SAT solver in Coq. In: Proc. Emerging Trends of TPHOLs (2008)","key":"18_CR13"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","volume":"43","author":"F. Mari\u0107","year":"2009","unstructured":"Mari\u0107, F.: Formalization and implementation of modern SAT solvers. J. Automated Reasoning\u00a043(1), 81\u2013119 (2009)","journal-title":"J. Automated Reasoning"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Moskal","year":"2008","unstructured":"Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 486\u2013500. Springer, Heidelberg (2008)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-75221-9_24","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"M. Penicka","year":"2007","unstructured":"Penicka, M.: Formal approach to railway applications. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol.\u00a04700, pp. 504\u2013520. Springer, Heidelberg (2007)"},{"key":"18_CR17","first-page":"129","volume-title":"Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M.J.C., Herbert, J., van Tassel, J.: Experience with embedding hardware description languages in HOL. In: Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pp. 129\u2013156. North-Holland, Amsterdam (1992)"},{"issue":"1","key":"18_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"18_CR19","volume-title":"Artificial Intelligence: A Modern Approach","author":"S.J. Russell","year":"2003","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice Hall, Englewood Cliffs (2003)","edition":"2"},{"unstructured":"SAT 2007 Competition (2007), http:\/\/www.cril.univ-artois.fr\/SAT07\/results\/globalbysolver.php?idev=11&det=1","key":"18_CR20"},{"unstructured":"SAT 2007 Competition - Phase 2 (2007), http:\/\/users.soe.ucsc.edu\/~avg\/ProofChecker\/cert-poster-sat07.pdf","key":"18_CR21"},{"issue":"1-2","key":"18_CR22","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","volume":"121","author":"D.S. Scott","year":"1993","unstructured":"Scott, D.S.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theor. Comput. Sci.\u00a0121(1-2), 411\u2013440 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-88387-6_3","volume-title":"Automated Technology for Verification and Analysis","author":"N. Shankar","year":"2008","unstructured":"Shankar, N.: Trust and Automation in Verification Tools. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 4\u201317. Springer, Heidelberg (2008)"},{"unstructured":"Smith, D.R., Westfold, S.J.: Synthesis of propositional satisfiability solvers. Technical report, Kestrel Institute (April 2008)","key":"18_CR24"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-72788-0_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Van Gelder","year":"2007","unstructured":"Van Gelder, A.: Verifying propositional unsatisfiability: Pitfalls to avoid. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 328\u2013333. Springer, Heidelberg (2007)"},{"unstructured":"Weber, T.: Efficiently checking propositional resolution proofs in Isabelle\/HOL. In: 6th Intl. Workshop Implementation of Logics, Phnom Penh 2006 (2006)","key":"18_CR26"},{"unstructured":"Weber, T., Amjad, H.: Private communication","key":"18_CR27"},{"issue":"1","key":"18_CR28","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic\u00a07(1), 26\u201340 (2009)","journal-title":"J. Applied Logic"},{"key":"18_CR29","first-page":"10880","volume-title":"Proc. Design, Automation and Test in Europe","author":"L. Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Proc. Design, Automation and Test in Europe, pp. 10880\u201310885. IEEE, Los Alamitos (2003)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14808-8_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:57:44Z","timestamp":1606186664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14808-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642148071","9783642148088"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14808-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}