Advertisement

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

  • Yeting Ge
  • Leonardo de Moura
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

Quantifier reasoning in Satisfiability Modulo Theories (SMT) is a long-standing challenge. The practical method employed in modern SMT solvers is to instantiate quantified formulas based on heuristics, which is not refutationally complete even for pure first-order logic. We present several decidable fragments of first order logic modulo theories. We show how to construct models for satisfiable formulas in these fragments. For richer undecidable fragments, we discuss conditions under which our procedure is refutationally complete. We also describe useful heuristics based on model checking for prioritizing or avoiding instantiations.

Keywords

Function Symbol Predicate Symbol Ground Term Uninterpreted Function Intended Structure 
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.
    Halpern, J.Y.: Presburger Arithmetic with unary predicates is \(\Pi_1^1\) Complete. Journal of Symbolic Logic 56, 637–642 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Deharbe, D., Ranise, S.: Satisfiability solving for software verification. International Journal on Software Tools Technology Transfer (2008) (to appear)Google Scholar
  3. 3.
    de Moura, L.M., Bjørner, N.: Efficient E-Matching for SMT Solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167–182. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning 1, 333–355 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167–182. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Flanagan, C., Joshi, R., 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
  7. 7.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52 (2005)Google Scholar
  9. 9.
    Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002. ACM, New York (2002)Google Scholar
  11. 11.
    Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 17–31. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Aiken, A.: Set Constraints: Results, Applications, and Future Directions. In: Second Workshop on the Principles and Practice of Constraint Programming (1994)Google Scholar
  14. 14.
    Ge, Y., de Moura, L.: Complete instantiation for quantified SMT formulas. Technical report, Microsoft Research (2009)Google Scholar
  15. 15.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    de Moura, L., 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
  17. 17.
    Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality. Presentation at Dagstuhl Seminar 05431 on Deduction and Applications (2005)Google Scholar
  18. 18.
    Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Fontaine, P., Gribomont, E.P.: Decidability of invariant validation for paramaterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 97–112. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Yeting Ge
    • 1
  • Leonardo de Moura
    • 2
  1. 1.Department of Computer ScienceNew York UniversityUSA
  2. 2.Microsoft Research, One Microsoft WayRedmondUSA

Personalised recommendations