Advertisement

Abstract

Modern Satisfiability Modulo Theories (SMT) solvers are used in a wide variety of software and hardware verification applications. Proof producing SMT solvers are very desirable as they increase confidence in the solver and ease debugging/profiling, while allowing for scenarios like Proof-Carrying Code (PCC). However, the size of typical proofs generated by SMT solvers poses a problem for the existing systems, up to the point where proof checking consumes orders of magnitude more computer resources than proof generation. In this paper we show how this problem can be addressed using a simple term rewriting formalism, which is used to encode proofs in a natural deduction style. We formally prove soundness of our rules and evaluate an implementation of the term rewriting engine on a set of proofs generated from industrial benchmarks. The modest memory and CPU time requirements of the implementation allow for proof checking even on a small PDA device, paving a way for PCC on such devices.

Keywords

Concrete Syntax Proof Tree Proof Rule Empty Clause Proof Check 
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.

References

  1. 1.
  2. 2.
    Barrett, C., Berezin, S.: CVC Lite: A new implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)Google Scholar
  3. 3.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001)Google Scholar
  4. 4.
    Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In: Second Automated Formal Methods workshop series (AFM 2007), Atlanta, Georgia, USA (November 2007)Google Scholar
  5. 5.
    de Bruijn, N.G.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34(5), 381–392 (1972)Google Scholar
  6. 6.
    de Moura, L., Bjorner, N.: Efficient E-matching for SMT solvers. In: Proceedings of the 21st International Conference on Automated Deduction (CADE-21), Springer, Heidelberg (to appear, 2007)Google Scholar
  7. 7.
    de Nivelle, H.: Implementing the clausal normal form transformation with proof generation. In: fourth workshop on the implementation of logics, Almaty, Kazachstan, University of Liverpool, University of Manchester, pp. 69–83 (2003)Google Scholar
  8. 8.
    de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Information and Computation 199(1), 24–54 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS 1987, Ithaca, NY, USA, June, 22–25, 1987, pp. 194–204. IEEE Computer Society Press, New York (1987)Google Scholar
  11. 11.
    Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming (1997)Google Scholar
  12. 12.
    McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: Armando, A., Cimatti, A. (eds.) Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), Edinburgh, Scotland, January 2006. Electronic Notes in Theoretical Computer Science, vol. 144(2), pp. 43–51. Elsevier, Amsterdam (2006)Google Scholar
  13. 13.
    Necula, G.C.: Proof-carrying code. In: Conference Record of POPL 1997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 106–119 (1997)Google Scholar
  14. 14.
    SMT-LIB: The Satisfiability Modulo Theories Library. http://www.smt-lib.org/
  15. 15.
    Stump, A., Dill, D.: Faster Proof Checking in the Edinburgh Logical Framework. In: 18th International Conference on Automated Deduction (2002)Google Scholar
  16. 16.
    Zeller, M., Stump, A., Deters, M.: A signature compiler for the Edinburgh Logical Framework. In: Proceedings of International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Michał Moskal
    • 1
  1. 1.University of WrocławPoland

Personalised recommendations