{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:55:05Z","timestamp":1725519305144},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540883869"},{"type":"electronic","value":"9783540883876"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88387-6_3","type":"book-chapter","created":{"date-parts":[[2008,10,10]],"date-time":"2008-10-10T01:42:45Z","timestamp":1223602965000},"page":"4-17","source":"Crossref","is-referenced-by-count":13,"title":["Trust and Automation in Verification Tools"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR2","volume-title":"The Correctness Problem in Computer Science","author":"R.S. Boyer","year":"1981","unstructured":"Boyer, R.S., Moore, J.S.: Metafunctions: Proving them correct and using them efficiently as new proof procedures. In: Boyer, R.S., Moore, J.S. (eds.) The Correctness Problem in Computer Science. Academic Press, London (1981)"},{"issue":"8","key":"3_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"3_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986), http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPRL\/"},{"unstructured":"Cornes, C., Courant, J., Filliatre, J.C., Huet, G., Manoury, P., Paulin-Mohring, C., Munoz, C., Murthy, C., Parent, C., Saibi, A., Werner, B.: The Coq proof assistant reference manual, version 5.10. Technical report, INRIA, Rocquencourt, France (February 1995)","key":"3_CR6"},{"key":"3_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/11591191_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Chaieb","year":"2005","unstructured":"Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for Presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 367\u2013380. Springer, Heidelberg (2005)"},{"unstructured":"Davis, J.: The Milawa rewriter and an ACL2 proof of its soundness. In: Gamboa, R., Sawada, J., Cowles, J. (eds.) Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications (2007)","key":"3_CR8"},{"key":"3_CR9","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Symposium on Automatic Demonstration","author":"N.G. Bruijn de","year":"1970","unstructured":"de Bruijn, N.G.: The mathematical language AUTOMATH, its usage and some of its extensions. In: Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol.\u00a0125, pp. 29\u201361. Springer, Berlin (1970)"},{"key":"3_CR10","first-page":"589","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project AUTOMATH. In: Seldin, J.P., Hindley, J.R. (eds.) Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 589\u2013606. Academic Press, New York (1980)"},{"key":"3_CR11","first-page":"78","volume":"60","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Gurevich, Y., Voronkov, A.: Herbrand\u2019s theorem and equational reasoning: Problems and solutions. Bulletin of the EATCS\u00a060, 78\u201396 (1996)","journal-title":"Bulletin of the EATCS"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-540-73368-3_5","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Dutertre, B., Shankar, N.: A tutorial on satisfiability modulo theories. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 20\u201336. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based proof search. In: Robinson, Voronkov. (eds.) [RV01], pp. 611\u2013706","key":"3_CR14","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proceedings of SAT 2003 (2003)","key":"3_CR15","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"3_CR16","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. Gelder Van","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)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993), http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/","key":"3_CR17"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"unstructured":"Harrison, J.: Formalized mathematics. Technical Report TUCS-TR-36, Turku Centre for Computer Science, Finland, August 14 (1996)","key":"3_CR19"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996), http:\/\/www.cl.cam.ac.uk\/jrh13\/hol-light\/index.html"},{"key":"3_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 177\u2013191. Springer, Heidelberg (2006)"},{"unstructured":"Knoblock, T.B., Constable, R.L.: Formalizing metareasoning in type theory. In: IEEE Symposium on Logic in Computer Science, Cambridge, MA (1986)","key":"3_CR22"},{"key":"3_CR23","first-page":"165","volume-title":"Fault Tolerant Computing Symposium 16","author":"J.C. Knight","year":"1986","unstructured":"Knight, J.C., Leveson, N.G.: An empirical study of failure probabilities in multi-version software. In: Fault Tolerant Computing Symposium 16, Vienna, Austria, July 1986, pp. 165\u2013170. IEEE Computer Society, Los Alamitos (1986)"},{"key":"3_CR24","series-title":"Advances in Formal Methods","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods, vol.\u00a03. Kluwer, Dordrecht (2000)"},{"unstructured":"Luo, Z., Pollack, R.: The LEGO proof development system: A user\u2019s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (1992)","key":"3_CR25"},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","volume":"144","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-light and CVC lite. Electr. Notes Theor. Comput. Sci\u00a0144(2), 43\u201351 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-44867-5_18","volume-title":"Experimental and Efficient Algorithms","author":"K. Mehlhorn","year":"2003","unstructured":"Mehlhorn, K.: The reliable algorithmic software challenge RASC. In: Jansen, K., Margraf, M., Mastrolli, M., Rolim, J.D.P. (eds.) WEA 2003. LNCS, vol.\u00a02647, p. 222. Springer, Heidelberg (2003)"},{"unstructured":"Dale, A.: Miller. Proofs in Higher-order Logic. PhD thesis, Carnegie-Mellon University (August 1983)","key":"3_CR28"},{"key":"3_CR29","volume-title":"Selected Papers on Automath","author":"R.P. Nederpelt","year":"1994","unstructured":"Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C.: Selected Papers on Automath. North-Holland, Amsterdam (1994)"},{"issue":"2","key":"3_CR30","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering\u00a021(2), 107\u2013125 (1995), http:\/\/pvs.csl.sri.com","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"3_CR32","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/SEFM.2006.24","volume-title":"Fourth International Conference on Software Engineering and Formal Methods (SEFM)","author":"J. Rushby","year":"2006","unstructured":"Rushby, J.: Harnessing disruptive innovation in formal verification. In: Van Hung, D., Pandya, P. (eds.) Fourth International Conference on Software Engineering and Formal Methods (SEFM), Pune, India, September 2006, pp. 21\u201328. IEEE Computer Society, Los Alamitos (2006)"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)","key":"3_CR33"},{"issue":"4","key":"3_CR34","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF00244278","volume":"1","author":"N. Shankar","year":"1985","unstructured":"Shankar, N.: Towards mechanical metamathematics. Journal of Automated Reasoning\u00a01(4), 407\u2013434 (1985)","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/11590156_4","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"N. Shankar","year":"2005","unstructured":"Shankar, N.: Inference systems for logical algorithms. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 60\u201378. Springer, Heidelberg (2005)"},{"key":"3_CR36","volume-title":"Mathematical Logic","author":"J.R. Shoenfield","year":"1967","unstructured":"Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)"},{"key":"3_CR37","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/S0049-237X(08)71123-6","volume-title":"The Handbook of Mathematical Logic","author":"C. Smorynski","year":"1978","unstructured":"Smorynski, C.: The incompleteness theorems. In: Barwise, J. (ed.) The Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol.\u00a090, pp. 821\u2013865. North-Holland, Amsterdam (1978)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 1\u201318. Springer, Heidelberg (2002)"},{"unstructured":"Shankar, N., Sorea, M.: Counterexample-driven model checking. Technical Report SRI-CSL-03-04, SRI International Computer Science Laboratory (2003)","key":"3_CR39"},{"unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver (submitted for publication, 2008)","key":"3_CR40"},{"key":"3_CR41","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BFb0054271","volume-title":"Automated Deduction - CADE-15","author":"L. Th\u00e9ry","year":"1998","unstructured":"Th\u00e9ry, L.: A certified version of Buchberger\u2019s algorithm. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 349\u2013364. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic (July 2007) (to appear), http:\/\/dx.doi.org\/10.1016\/j.jal.2007.07.003","key":"3_CR42","DOI":"10.1016\/j.jal.2007.07.003"},{"issue":"1 and 2","key":"3_CR43","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R.W. Weyhrauch","year":"1980","unstructured":"Weyhrauch, R.W.: Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence\u00a013(1 and 2), 133\u2013170 (1980)","journal-title":"Artificial Intelligence"},{"key":"3_CR44","first-page":"1173","volume-title":"IJCAI 2003, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence","author":"R. Williams","year":"2003","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Gottlob, G., Walsh, T. (eds.) IJCAI 2003, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, pp. 1173\u20131178. Morgan Kaufmann, San Francisco (2003)"},{"issue":"3-4","key":"3_CR45","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1023\/A:1021983302516","volume":"29","author":"F. Wiedijk","year":"2002","unstructured":"Wiedijk, F.: A new implementation of Automath. J. Autom. Reasoning\u00a029(3-4), 365\u2013387 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR46","first-page":"10880","volume-title":"DATE","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: DATE, pp. 10880\u201310885. IEEE Computer Society, Los Alamitos (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88387-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T10:45:39Z","timestamp":1557830739000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88387-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883869","9783540883876"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88387-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}