A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover

  • K. Rustan M. Leino
  • Madan Musuvathi
  • Xinming Ou
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


Lazy proof explication is a theorem-proving architecture that allows a combination of Nelson-Oppen-style decision procedures to leverage a SAT solver’s ability to perform propositional reasoning efficiently. The SAT solver finds ways to satisfy a given formula propositionally, while the various decision procedures perform theory reasoning to block propositionally satisfied instances that are not consistent with the theories. Supporting quantifiers in this architecture poses a challenge as quantifier instantiations can dynamically introduce boolean structure in the formula, requiring a tighter interleaving between propositional and theory reasoning.

This paper proposes handling quantifiers by using two SAT solvers, thereby separating the propositional reasoning of the input formula from that of the instantiated formulas. This technique can then reduce the propositional search space, as the paper demonstrates. The technique can use off-the-shelf SAT solvers and requires only that the theories are checkpointable.


Decision Procedure Theorem Prover Theory Reasoning Satisfying Assignment Original 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.


  1. 1.
    Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)CrossRefGoogle Scholar
  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)CrossRefGoogle Scholar
  3. 3.
    de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002 (May 2002)Google Scholar
  4. 4.
    Déharbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Proc. of the International Conference on Software Engineering and Formal Methods (SEFM 2003), Camberra, Australia (September 2003)Google Scholar
  5. 5.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (July 2003)Google Scholar
  6. 6.
    Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)Google Scholar
  7. 7.
    Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical Report HPL-2004-199, HP Labs (2004)Google Scholar
  9. 9.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)CrossRefGoogle Scholar
  10. 10.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Nelson, C.G.: Techniques for Program Verification. PhD thesis, Stanford University, 1980. Also available as Xerox PARC technical report CSL-81-10 (1981)Google Scholar
  12. 12.
    Nelson, G., Oppen, D.C.: Simplification by coorperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)zbMATHCrossRefGoogle Scholar
  13. 13.
    Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Commun 15(2), 91–110 (2002)zbMATHGoogle Scholar
  14. 14.
    Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • K. Rustan M. Leino
    • 1
  • Madan Musuvathi
    • 1
  • Xinming Ou
    • 2
  1. 1.Microsoft ResearchRedmondUSA
  2. 2.Princeton UniversityPrincetonUSA

Personalised recommendations