Satisfiability Modulo Theories

Chapter

Abstract

Satisfiability Modulo Theories (SMT) refers to the problem of determining whether a first-order formula is satisfiable with respect to some logical theory. Solvers based on SMT are used as back-end engines in model-checking applications such as bounded, interpolation-based, and predicate-abstraction-based model checking. After a brief illustration of these uses, we survey the predominant techniques for solving SMT problems with an emphasis on the lazy approach, in which a propositional satisfiability (SAT) solver is combined with one or more theory solvers. We discuss the architecture of a lazy SMT solver, give examples of theory solvers, show how to combine such solvers modularly, and mention several extensions of the lazy approach. We also briefly describe the eager approach in which the SMT problem is reduced to a SAT problem. Finally, we discuss how the basic framework for determining satisfiability can be extended with additional functionality such as producing models, proofs, unsatisfiable cores, and interpolants.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954) MATHGoogle Scholar
  2. 2.
    Amjad, H.: A compressing translation from propositional resolution to natural deduction. In: Konev, B., Wolter, F. (eds.) Intl. Symp. on Frontiers of Combining Systems (FroCoS). LNCS, vol. 4720, pp. 88–102. Springer, Heidelberg (2007) Google Scholar
  3. 3.
    Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) European Conf. on Planning (ECP). LNCS, vol. 1809, pp. 97–108. Springer, Heidelberg (2000) Google Scholar
  4. 4.
    Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 3925, pp. 146–162. Springer, Heidelberg (2006) MATHGoogle Scholar
  5. 5.
    Audemard, G., Bertoli, P., Cimatti, A., Korniłowicz, A., Sebastiani, R.: A SAT-based approach for solving formulas over Boolean and linear mathematical propositions. In: Voronkov, A. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 2392, pp. 195–210. Springer, Heidelberg (2002) Google Scholar
  6. 6.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) MATHGoogle Scholar
  7. 7.
    Babić, D.: Exploiting structure for scalable software verification. Ph.D. thesis, University of British Columbia (2008) Google Scholar
  8. 8.
    Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 203–213. ACM, New York (2001) Google Scholar
  9. 9.
    Barrett, C., Berezin, S.: A proof-producing Boolean search engine. In: Intl. Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) (2003) Google Scholar
  10. 10.
    Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011) Google Scholar
  11. 11.
    Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 4246, pp. 512–526. Springer, Heidelberg (2006) MATHGoogle Scholar
  12. 12.
    Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009) Google Scholar
  13. 13.
    Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput. 3, 21–46 (2007) MathSciNetMATHGoogle Scholar
  14. 14.
    Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.smtlib.org
  15. 15.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010) Google Scholar
  16. 16.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Tech. rep., Department of Computer Science, University of Iowa (2010) Google Scholar
  17. 17.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007) Google Scholar
  18. 18.
    Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Chawla, B.R., Bryant, R.E., Rabaey, J.M. (eds.) Design Automation Conf. (DAC), pp. 522–527. ACM, New York (1998) Google Scholar
  19. 19.
    Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 236–249 (2002) Google Scholar
  20. 20.
    Barrett, C.W., de Moura, L., Stump, A.: Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). J. Autom. Reason. 35(4), 373–390 (2005) MATHGoogle Scholar
  21. 21.
    Berezin, S., Ganesh, V., Dill, D.L.: An online proof-producing decision procedure for mixed-integer linear arithmetic. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 521–536. Springer, Heidelberg (2003) Google Scholar
  22. 22.
    Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) MATHGoogle Scholar
  23. 23.
    Biere, A., Kroening, D.: SAT-based model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  24. 24.
    Bjørner, N., de Moura, L.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 4603, pp. 183–198. Springer, Heidelberg (2007) Google Scholar
  25. 25.
    Bjørner, N., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1384, pp. 376–392. Springer, Heidelberg (1998) Google Scholar
  26. 26.
    Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT/BPR), pp. 1–5. ACM, New York (2008) Google Scholar
  27. 27.
    Bofill, M., Nieuwenhuis, R., Oliveras, A., Carbonell, E.R., Rubio, A.: A write-based solver for SAT modulo the theory of arrays. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 1–8. IEEE, Piscataway (2008) Google Scholar
  28. 28.
    Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) Intl. Conf. on Interactive Theorem Proving (ITP). LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010) Google Scholar
  29. 29.
    Bouton, T., De Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009) Google Scholar
  30. 30.
    Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., Sebastiani, R., van Rossum, P.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576. Springer, Heidelberg (2005) Google Scholar
  31. 31.
    Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient theory combination via Boolean search. Inf. Comput. 204(10), 1411–1596 (2006) MathSciNetMATHGoogle Scholar
  32. 32.
    Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 317–333 (2005) MATHGoogle Scholar
  33. 33.
    Bradley, A., Manna, Z., Sipma, H.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006) Google Scholar
  34. 34.
    Brain, M., D’Silva, V., Haller, L., Griggio, A., Kroening, D.: An abstract interpretation of DPLL(T). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 7737, pp. 455–475. Springer, Heidelberg (2013) MATHGoogle Scholar
  35. 35.
    Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. In: Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT/BPR), pp. 6–11. ACM, New York (2008) Google Scholar
  36. 36.
    Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009) Google Scholar
  37. 37.
    Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT(BV) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 547–560. Springer, Heidelberg (2007) Google Scholar
  38. 38.
    Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1–2), 63–99 (2009) MathSciNetMATHGoogle Scholar
  39. 39.
    Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010) Google Scholar
  40. 40.
    Bruttomesso, R., Rollini, S., Sharygina, N., Tsitovich, A.: Flexible interpolation with local proof transformations. In: Scheffer, L., Phillips, J.R., Hu, A.J. (eds.) Intl. Conf. on Computer-Aided Design, pp. 770–777. IEEE, Piscataway (2010) Google Scholar
  41. 41.
    Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: Roychowdhury, J.S. (ed.) Intl. Conf. on Computer-Aided Design, pp. 13–20. ACM, New York (2009) Google Scholar
  42. 42.
    Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 106–122. Springer, Heidelberg (2002) Google Scholar
  43. 43.
    Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 470–482. Springer, Heidelberg (1999) Google Scholar
  44. 44.
    Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007) Google Scholar
  45. 45.
    Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings. In: Intl. Workshop on Constraints in Formal Verification (CFV) (2002) Google Scholar
  46. 46.
    Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4), 604–627 (2002) MathSciNetMATHGoogle Scholar
  47. 47.
    Cantone, D., Zarba, C.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) Automated Deduction in Classical and Non-classical Logics. LNCS, vol. 1761, pp. 492–495. Springer, Heidelberg (2000) Google Scholar
  48. 48.
    Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) MATHGoogle Scholar
  49. 49.
    Chatterjee, S., Lahiri, S., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007) MATHGoogle Scholar
  50. 50.
    Cherkassy, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: Díaz, J., Serna, M.J. (eds.) Annual European Symp. on Algorithms (ESA). LNCS, vol. 1136, pp. 349–363. Springer, Heidelberg (1996) Google Scholar
  51. 51.
    Christ, J., Hoenicke, J., Nutz, A.: SMTinterpol: an interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012) Google Scholar
  52. 52.
    Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 7795, pp. 124–138. Springer, Heidelberg (2013) Google Scholar
  53. 53.
    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013) MATHGoogle Scholar
  54. 54.
    Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 397–412. Springer, Berlin (2008) Google Scholar
  55. 55.
    Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 1–54 (2010) MathSciNetMATHGoogle Scholar
  56. 56.
    Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. 40(1), 701–728 (2011) MathSciNetMATHGoogle Scholar
  57. 57.
    Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001) MATHGoogle Scholar
  58. 58.
    Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006) MATHGoogle Scholar
  59. 59.
    Cotton, S., Maler, O.: Satisfiability modulo theory chains with DPLL(T). Tech. rep., Verimag (2006) Google Scholar
  60. 60.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269–285 (1957) MathSciNetMATHGoogle Scholar
  61. 61.
    Cyrluk, D., Möller, O., Rueß, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997) Google Scholar
  62. 62.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962) MathSciNetMATHGoogle Scholar
  63. 63.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) MathSciNetMATHGoogle Scholar
  64. 64.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005) MathSciNetMATHGoogle Scholar
  65. 65.
    Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Maler, A.B.O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 233–247. Springer, Heidelberg (2009) Google Scholar
  66. 66.
    Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980) MathSciNetMATHGoogle Scholar
  67. 67.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006) Google Scholar
  68. 68.
    Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. rep., CSL, SRI International (2006) Google Scholar
  69. 69.
    Dutertre, B., de Moura, L.: The YICES SMT solver. Tech. rep., SRI International (2006) Google Scholar
  70. 70.
    Echenim, M., Peltier, N.: An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 293–362 (2010) MathSciNetMATHGoogle Scholar
  71. 71.
    Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Cambridge (2001) MATHGoogle Scholar
  72. 72.
    Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003) Google Scholar
  73. 73.
    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.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3920, pp. 167–181. Springer, Berlin (2006) Google Scholar
  74. 74.
    Fröhlich, A., Kovásznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) Computer Science: Theory and Applications. LNCS, vol. 7913, pp. 378–390. Springer, Heidelberg (2013) Google Scholar
  75. 75.
    Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground interpolation for the theory of equality. In: Kowalewski, S., Philippou, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 5505, pp. 413–427. Springer, Heidelberg (2009) MATHGoogle Scholar
  76. 76.
    Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007) Google Scholar
  77. 77.
    Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.D.: Fast decision procedures. In: Alur, R., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004) Google Scholar
  78. 78.
    Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Symp. on Logic in Computer Science, vol. LICS, pp. 55–64. IEEE, Piscataway (2003) Google Scholar
  79. 79.
    Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 4246, pp. 497–511. Springer, Heidelberg (2006) Google Scholar
  80. 80.
    Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 7898, pp. 208–214. Springer, Berlin (2013) Google Scholar
  81. 81.
    Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2008) Google Scholar
  82. 82.
    Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 4603, pp. 167–182. Springer, Heidelberg (2007) Google Scholar
  83. 83.
    Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009) Google Scholar
  84. 84.
    Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3–4), 221–249 (2005) MathSciNetMATHGoogle Scholar
  85. 85.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 4603, pp. 362–378. Springer, Heidelberg (2007) Google Scholar
  86. 86.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 5195, pp. 67–82. Springer, Heidelberg (2008) Google Scholar
  87. 87.
    Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 1–54 (2008) MathSciNetMATHGoogle Scholar
  88. 88.
    Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 6173, pp. 22–29. Springer, Heidelberg (2010) Google Scholar
  89. 89.
    Goel, A., Krstić, S., Fuchs, A.: Deciding array formulas with frugal axiom instantiation. In: Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT/BPR), pp. 12–17. ACM, New York (2008) Google Scholar
  90. 90.
    Goel, A., Krstić, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 5663, pp. 183–198. Springer, Heidelberg (2009) Google Scholar
  91. 91.
    Griggio, A.: An effective SMT engine for formal verification. Ph.D. thesis, DISI, University of Trento (2009) Google Scholar
  92. 92.
    Griggio, A.: A practical approach to SMT(LA(Z)). In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010) Google Scholar
  93. 93.
    Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 109–117. IEEE, Piscataway (2008) Google Scholar
  94. 94.
    Jha, S.K., Limaye, R.S., Seshia, S.A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic. Tech. rep., EECS Department, University of California, Berkeley Google Scholar
  95. 95.
    Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005) Google Scholar
  96. 96.
    Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  97. 97.
    Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010) Google Scholar
  98. 98.
    Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Formal Methods in Computer Aided Design (FMCAD), pp. 173–180. IEEE, Piscataway (2013) Google Scholar
  99. 99.
    Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012) Google Scholar
  100. 100.
    Kapur, D., Majumdar, R., Zarba, C.: Interpolation for data structures. In: Young, M., Devanbu, P.T. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp. 105–116. ACM, New York (2006) Google Scholar
  101. 101.
    Kapur, D., Zarba, C.G.: A reduction approach to decision procedures. Tech. rep., University of New Mexico (2005) Google Scholar
  102. 102.
    Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Rothermel, G., Dillon, L.K. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp. 105–116. ACM, New York (2009) Google Scholar
  103. 103.
    Kim, H., Somenzi, F.: Finite instantiations for integer difference logic. In: Formal Methods in Computer Aided Design (FMCAD), pp. 31–38. IEEE, Piscataway (2006) Google Scholar
  104. 104.
    King, T., Barrett, C., Dutertre, B.: Sum of infeasibility simplex for SMT. In: Formal Methods in Computer Aided Design (FMCAD), pp. 189–196. IEEE, Piscataway (2013) Google Scholar
  105. 105.
    Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 5195, pp. 292–298. Springer, Heidelberg (2008) Google Scholar
  106. 106.
    Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol. 5732, pp. 509–523. Springer, Heidelberg (2009) Google Scholar
  107. 107.
    Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008) MATHGoogle Scholar
  108. 108.
    Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) Intl. Symp. on Frontiers of Combining Systems (FroCoS). LNCS, vol. 4720, pp. 1–27. Springer, Heidelberg (2007) Google Scholar
  109. 109.
    Krstić, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 618–631. Springer, Heidelberg (2007) Google Scholar
  110. 110.
    Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M., O’Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 2517, pp. 142–159. Springer, Heidelberg (2002) Google Scholar
  111. 111.
    Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 3632, pp. 99–115. Springer, Heidelberg (2005) Google Scholar
  112. 112.
    Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads: From Panacea to Foundational Support. LNCS, vol. 2757, pp. 381–422. Springer, Heidelberg (2003) Google Scholar
  113. 113.
    Manolios, P., Srinivasan, S., Vroon, D.B.: The bit-level analysis tool. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 303–306. Springer, Heidelberg (2007) Google Scholar
  114. 114.
    Manzano, M.: Introduction to many-sorted logic. In: Meinke, K., Tucker, J.V. (eds.) Many-Sorted Logic and Its Applications, pp. 3–86. Wiley, New York (1993) Google Scholar
  115. 115.
    McMillan, K.: Interpolation and SAT-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) Google Scholar
  116. 116.
    McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005) Google Scholar
  117. 117.
    McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005) MathSciNetMATHGoogle Scholar
  118. 118.
    McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  119. 119.
    McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 462–476 (2009) Google Scholar
  120. 120.
    Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 486–500. Springer, Heidelberg (2008) Google Scholar
  121. 121.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 4963, pp. 337–340. Springer, Heidelberg (2008) Google Scholar
  122. 122.
    de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer Aided Design (FMCAD), pp. 45–52. IEEE, Piscataway (2009) Google Scholar
  123. 123.
    de Moura, L., Bjørner, N.S.: Model-based theory combination. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2007) Google Scholar
  124. 124.
    de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Intl. Symp. on the Theory and Applications of Satisfiability Testing (SAT) (2002) Google Scholar
  125. 125.
    de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003) MATHGoogle Scholar
  126. 126.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. Trans. Program. Lang. Syst. 1(2), 245–257 (1979) MATHGoogle Scholar
  127. 127.
    Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980) MathSciNetMATHGoogle Scholar
  128. 128.
    Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005) Google Scholar
  129. 129.
    Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006) MATHGoogle Scholar
  130. 130.
    Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557–580 (2007) MathSciNetMATHGoogle Scholar
  131. 131.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 3452, pp. 36–50. Springer, Heidelberg (2005) MATHGoogle Scholar
  132. 132.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) MathSciNetMATHGoogle Scholar
  133. 133.
    Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2009) Google Scholar
  134. 134.
    Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291–302 (1980) MathSciNetMATHGoogle Scholar
  135. 135.
    Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods Symp. (NFM). LNCS, vol. 6617, pp. 298–312. Springer, Heidelberg (2011) Google Scholar
  136. 136.
    Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D., Zuck, L.D. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI), vol. 4905, pp. 218–232. Springer, Heidelberg (2008) Google Scholar
  137. 137.
    Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small domains instantiations. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 687–688. Springer, Heidelberg (1999) Google Scholar
  138. 138.
    Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves, Warsaw, pp. 92–101 (1929) Google Scholar
  139. 139.
    Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997) MathSciNetMATHGoogle Scholar
  140. 140.
    Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Martin, J.L. (ed.) Conf. on Supercomputing (SC), pp. 4–13. IEEE/ACM, Piscataway/New York (1991) Google Scholar
  141. 141.
    Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) Intl. Symp. on Frontiers of Combining Systems (FroCoS). LNCS, vol. 3717, pp. 48–64. Springer, Heidelberg (2005) MATHGoogle Scholar
  142. 142.
    Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013) Google Scholar
  143. 143.
    Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 7898, pp. 377–391. Springer, Heidelberg (2013) Google Scholar
  144. 144.
    Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010) Google Scholar
  145. 145.
    Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J. Symb. Comput. 45, 1212–1233 (2010) MathSciNetMATHGoogle Scholar
  146. 146.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986) MATHGoogle Scholar
  147. 147.
    Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3–4), 141–224 (2007) MathSciNetMATHGoogle Scholar
  148. 148.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000) Google Scholar
  149. 149.
    Sheini, H.M., Sakallah, K.A.: A scalable method for solving satisfiability of integer linear arithmetic logic. In: Bacchus, F., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 3569, pp. 241–256. Springer, Heidelberg (2005) MATHGoogle Scholar
  150. 150.
    Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 3632, pp. 219–234. Springer, Heidelberg (2005) Google Scholar
  151. 151.
    Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Aagaard, M., O’Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 2517, pp. 160–170. Springer, Heidelberg (2002) Google Scholar
  152. 152.
    Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 113–124. Springer, Heidelberg (2002) Google Scholar
  153. 153.
    Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Symp. on Logic in Computer Science, vol. LICS, pp. 29–37. IEEE, Piscataway (2001) Google Scholar
  154. 154.
    Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Form. Methods Syst. Des. 41(1), 91–118 (2013) MATHGoogle Scholar
  155. 155.
    Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215–225 (1975) MathSciNetMATHGoogle Scholar
  156. 156.
    Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Ianni, G., Flesca, S. (eds.) European Conf. on Logics in Artificial Intelligence (JELIA). LNCS, vol. 2424, pp. 308–319. Springer, Heidelberg (2002) Google Scholar
  157. 157.
    Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Intl. Workshop on Frontiers of Combining Systems (FroCoS), pp. 103–120. Kluwer Academic, Dordrecht (1996) MATHGoogle Scholar
  158. 158.
    Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291–353 (2003) MathSciNetMATHGoogle Scholar
  159. 159.
    Tinelli, C., Zarba, C.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J.A. (eds.) European Conf. on Logics in Artificial Intelligence (JELIA). Lecture Notes in Artificial Intelligence, vol. 3229, pp. 641–653. Springer, Heidelberg (2004) Google Scholar
  160. 160.
    Tinelli, C., Zarba, C.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209–238 (2005) MathSciNetMATHGoogle Scholar
  161. 161.
    Wang, C., Gupta, A., Ganai, M.: Predicate learning and selective theory deduction for a difference logic solver. In: Sentovich, E. (ed.) Design Automation Conf. (DAC), pp. 235–240. ACM, New York (2006) Google Scholar
  162. 162.
    Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 3632, pp. 353–368. Springer, Heidelberg (2005) Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Stanford UniversityStanfordUSA
  2. 2.The University of IowaIowa CityUSA

Personalised recommendations