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.
Chapter PDF
Similar content being viewed by others
Keywords
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
Fx7 web page, http://nemerle.org/fx7/
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)
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)
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)
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)
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)
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)
de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Information and Computation 199(1), 24–54 (2005)
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)
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)
Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming (1997)
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)
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)
SMT-LIB: The Satisfiability Modulo Theories Library. http://www.smt-lib.org/
Stump, A., Dill, D.: Faster Proof Checking in the Edinburgh Logical Framework. In: 18th International Conference on Automated Deduction (2002)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moskal, M. (2008). Rocket-Fast Proof Checking for SMT Solvers. In: Ramakrishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78800-3_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-78800-3_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78799-0
Online ISBN: 978-3-540-78800-3
eBook Packages: Computer ScienceComputer Science (R0)