Advertisement

Trust and Automation in Verification Tools

  • Natarajan Shankar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

On the one hand, we would like verification tools to feature powerful automation, but on the other hand, we also want to be able to trust the results with a high degree of confidence. The question of trust in verification tools has been debated for a long time. One popular way of achieving trust in verification tools is through proof generation. However, proof generation could hamstring both the functionality and the efficiency of the automation that can be built into these tools. We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach where the results of untrusted verifiers are checked by a trusted offline checker. The trusted checker is a verified reference kernel that contains a satisfiability solver to support the robust and efficient checking of untrusted tools.

Keywords

Proof System Conjunctive Normal Form Binary Decision Diagram Partial Assignment Conjunctive Normal Form Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BB04]
    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. 3114, pp. 515–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. [BM81]
    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)Google Scholar
  3. [Bry86]
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  4. [BT07]
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. [CAB+86]
    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/ Google Scholar
  6. [CCF+95]
    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)Google Scholar
  7. [CN05]
    Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for Presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 367–380. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. [Dav07]
    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)Google Scholar
  9. [dB70]
    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. 125, pp. 29–61. Springer, Berlin (1970)CrossRefGoogle Scholar
  10. [dB80]
    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–606. Academic Press, New York (1980)Google Scholar
  11. [DGV96]
    Degtyarev, A., Gurevich, Y., Voronkov, A.: Herbrand’s theorem and equational reasoning: Problems and solutions. Bulletin of the EATCS 60, 78–96 (1996)zbMATHGoogle Scholar
  12. [dMB08]
    de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  13. [dMDS07]
    de Moura, L., Dutertre, B., Shankar, N.: A tutorial on satisfiability modulo theories. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 20–36. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. [DV01]
    Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based proof search. In: Robinson, Voronkov. (eds.) [RV01], pp. 611–706Google Scholar
  15. [ES03]
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proceedings of SAT 2003 (2003)Google Scholar
  16. [Gel07]
    Van Gelder, A.: Verifying propositional unsatisfiability: Pitfalls to avoid. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 328–333. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. [GM93]
    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/ zbMATHGoogle Scholar
  18. [GMW79]
    Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)zbMATHGoogle Scholar
  19. [Har96a]
    Harrison, J.: Formalized mathematics. Technical Report TUCS-TR-36, Turku Centre for Computer Science, Finland, August 14 (1996)Google Scholar
  20. [Har96b]
    Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996), http://www.cl.cam.ac.uk/jrh13/hol-light/index.html CrossRefGoogle Scholar
  21. [Har06]
    Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 177–191. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  22. [KC86]
    Knoblock, T.B., Constable, R.L.: Formalizing metareasoning in type theory. In: IEEE Symposium on Logic in Computer Science, Cambridge, MA (1986)Google Scholar
  23. [KL86]
    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–170. IEEE Computer Society, Los Alamitos (1986)Google Scholar
  24. [KMM00]
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods, vol. 3. Kluwer, Dordrecht (2000)Google Scholar
  25. [LP92]
    Luo, Z., Pollack, R.: The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (1992)Google Scholar
  26. [MBG06]
    McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-light and CVC lite. Electr. Notes Theor. Comput. Sci 144(2), 43–51 (2006)CrossRefzbMATHGoogle Scholar
  27. [Meh03]
    Mehlhorn, K.: The reliable algorithmic software challenge RASC. In: Jansen, K., Margraf, M., Mastrolli, M., Rolim, J.D.P. (eds.) WEA 2003. LNCS, vol. 2647, p. 222. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  28. [Mil83]
    Dale, A.: Miller. Proofs in Higher-order Logic. PhD thesis, Carnegie-Mellon University (August 1983)Google Scholar
  29. [NGdV94]
    Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C.: Selected Papers on Automath. North-Holland, Amsterdam (1994)zbMATHGoogle Scholar
  30. [ORSvH95]
    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 21(2), 107–125 (1995), http://pvs.csl.sri.com CrossRefGoogle Scholar
  31. [Pau94]
    Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)CrossRefzbMATHGoogle Scholar
  32. [Rus06]
    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–28. IEEE Computer Society, Los Alamitos (2006)CrossRefGoogle Scholar
  33. [RV01]
    Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)zbMATHGoogle Scholar
  34. [Sha85]
    Shankar, N.: Towards mechanical metamathematics. Journal of Automated Reasoning 1(4), 407–434 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  35. [Sha05]
    Shankar, N.: Inference systems for logical algorithms. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 60–78. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  36. [Sho67]
    Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)zbMATHGoogle Scholar
  37. [Smo78]
    Smorynski, C.: The incompleteness theorems. In: Barwise, J. (ed.) The Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 90, pp. 821–865. North-Holland, Amsterdam (1978)CrossRefGoogle Scholar
  38. [SR02]
    Shankar, N., Rueß, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–18. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  39. [SS03]
    Shankar, N., Sorea, M.: Counterexample-driven model checking. Technical Report SRI-CSL-03-04, SRI International Computer Science Laboratory (2003)Google Scholar
  40. [SV08]
    Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver (submitted for publication, 2008)Google Scholar
  41. [Thé98]
    Théry, L.: A certified version of Buchberger’s algorithm. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 349–364. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  42. [WA07]
    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
  43. [Wey80]
    Weyhrauch, R.W.: Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence 13(1 and 2), 133–170 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  44. [WGS03]
    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–1178. Morgan Kaufmann, San Francisco (2003)Google Scholar
  45. [Wie02]
    Wiedijk, F.: A new implementation of Automath. J. Autom. Reasoning 29(3-4), 365–387 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  46. [ZM03]
    Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, pp. 10880–10885. IEEE Computer Society, Los Alamitos (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Natarajan Shankar
    • 1
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations