×

Satisfiability modulo theories. (English) Zbl 1392.68379

Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 305-343 (2018).
Summary: 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.
For the entire collection see [Zbl 1390.68001].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 1. Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954) · Zbl 0056.24505
[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) · Zbl 1148.68464
[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) · Zbl 1098.68693
[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) · Zbl 1178.68148
[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) · Zbl 1072.68562
[6] 6. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098
[7] 7. Babić, D.: Exploiting structure for scalable software verification. Ph.D. thesis, University of British Columbia (2008)
[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)
[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)
[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)
[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) · Zbl 1165.68480
[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)
[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) · Zbl 1129.68022
[14] 14. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010).
[15] 15. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010)
[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)
[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)
[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)
[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) · Zbl 1010.68531
[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) · Zbl 1104.68719
[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) · Zbl 1031.68584
[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) · Zbl 1183.68568
[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) · Zbl 1392.68232
[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) · Zbl 1213.68578
[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)
[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)
[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)
[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) · Zbl 1291.68328
[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)
[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) · Zbl 1081.68610
[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) · Zbl 1137.68578
[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) · Zbl 1087.68630
[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) · Zbl 1176.68116
[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) · Zbl 1426.68249
[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)
[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)
[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)
[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) · Zbl 1192.68627
[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)
[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) · Zbl 1317.68123
[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)
[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) · Zbl 1010.68522
[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) · Zbl 1046.68584
[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) · Zbl 1186.68281
[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)
[46] 46. Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4), 604-627 (2002) · Zbl 1365.68318
[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) · Zbl 0955.03015
[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) · Zbl 1392.68239
[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) · Zbl 1186.68108
[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) · Zbl 1379.68254
[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)
[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) · Zbl 1381.68152
[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) · Zbl 1381.68153
[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) · Zbl 1134.68402
[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) · Zbl 1351.68247
[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) · Zbl 1216.68241
[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) · Zbl 0985.68038
[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) · Zbl 1187.68537
[59] 59. Cotton, S., Maler, O.: Satisfiability modulo theory chains with DPLL(T). Tech. rep., Verimag (2006) · Zbl 1187.68537
[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) · Zbl 0079.24502
[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)
[62] 62. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394-397 (1962) · Zbl 0217.54002
[63] 63. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201-215 (1960) · Zbl 0212.34203
[64] 64. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365-473 (2005) · Zbl 1323.68462
[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) · Zbl 1242.65116
[66] 66. Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758-771 (1980) · Zbl 0458.68026
[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)
[68] 68. Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. rep., CSL, SRI International (2006)
[69] 69. Dutertre, B., de Moura, L.: The YICES SMT solver. Tech. rep., SRI International (2006)
[70] 70. Echenim, M., Peltier, N.: An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 293-362 (2010) · Zbl 1430.68401
[71] 71. Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Cambridge (2001) · Zbl 0992.03001
[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) · Zbl 1278.68259
[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) · Zbl 1180.68240
[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) · Zbl 1345.68172
[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) · Zbl 1234.68257
[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) · Zbl 1135.68472
[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) · Zbl 1103.68616
[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)
[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) · Zbl 1165.03315
[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) · Zbl 1381.68268
[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)
[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) · Zbl 1213.68376
[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) · Zbl 1242.68280
[84] 84. Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3-4), 221-249 (2005) · Zbl 1069.03008
[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) · Zbl 1213.68378
[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) · Zbl 1165.68406
[87] 87. Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 1-54 (2008) · Zbl 1407.03011
[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) · Zbl 1291.68257
[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)
[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) · Zbl 1250.68188
[91] 91. Griggio, A.: An effective SMT engine for formal verification. Ph.D. thesis, DISI, University of Trento (2009)
[92] 92. Griggio, A.: A practical approach to SMT(LA(Z)). In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010)
[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)
[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
[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) · Zbl 1081.68622
[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) · Zbl 1392.68253
[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) · Zbl 1306.68147
[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)
[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) · Zbl 1358.68257
[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)
[101] 101. Kapur, D., Zarba, C.G.: A reduction approach to decision procedures. Tech. rep., University of New Mexico (2005)
[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)
[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)
[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)
[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) · Zbl 1165.68462
[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) · Zbl 1336.68236
[107] 107. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008) · Zbl 1149.68071
[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) · Zbl 1148.68466
[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) · Zbl 1186.68297
[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) · Zbl 1019.68623
[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) · Zbl 1135.68556
[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) · Zbl 1274.68078
[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)
[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)
[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) · Zbl 1278.68184
[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) · Zbl 1087.68597
[117] 117. McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101-121 (2005) · Zbl 1079.68092
[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) · Zbl 1392.68260
[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) · Zbl 1242.68282
[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) · Zbl 1134.68492
[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)
[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)
[123] 123. de Moura, L., Bjørner, N.S.: Model-based theory combination. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2007) · Zbl 1277.03007
[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)
[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) · Zbl 1278.68199
[126] 126. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. Trans. Program. Lang. Syst. 1(2), 245-257 (1979) · Zbl 0452.68013
[127] 127. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356-364 (1980) · Zbl 0441.68111
[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) · Zbl 1081.68629
[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) · Zbl 1187.68558
[130] 130. Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557-580 (2007) · Zbl 1112.68116
[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) · Zbl 1109.68097
[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) · Zbl 1326.68164
[133] 133. Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2009)
[134] 134. Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291-302 (1980) · Zbl 0437.03007
[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)
[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) · Zbl 1138.68528
[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) · Zbl 1046.68605
[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) · JFM 56.0825.04
[139] 139. Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symb. Log. 62(3), 981-998 (1997) · Zbl 0945.03086
[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)
[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) · Zbl 1171.68439
[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)
[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) · Zbl 1381.68275
[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)
[145] 145. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J. Symb. Comput. 45, 1212-1233 (2010) · Zbl 1213.68389
[146] 146. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986) · Zbl 0665.90063
[147] 147. Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3-4), 141-224 (2007) · Zbl 1145.68501
[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)
[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) · Zbl 1128.68483
[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) · Zbl 1135.03330
[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) · Zbl 1019.68592
[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) · Zbl 1010.68168
[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)
[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) · Zbl 1284.68521
[155] 155. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215-225 (1975) · Zbl 0307.68029
[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) · Zbl 1013.68192
[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) · Zbl 0893.03001
[158] 158. Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291-353 (2003) · Zbl 1018.68033
[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) · Zbl 1111.68691
[160] 160. Tinelli, C., Zarba, C.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209-238 (2005) · Zbl 1108.03014
[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)
[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) · Zbl 1135.03331
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.