{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T13:39:56Z","timestamp":1774964396506,"version":"3.50.1"},"publisher-location":"Cham","reference-count":162,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_11","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"305-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":309,"title":["Satisfiability Modulo Theories"],"prefix":"10.1007","author":[{"given":"Clark","family":"Barrett","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"11_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954)"},{"key":"11_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-74621-8_6","volume-title":"Intl. Symp. on Frontiers of Combining Systems (FroCoS)","author":"H. Amjad","year":"2007","unstructured":"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.\u00a04720, pp.\u00a088\u2013102. Springer, Heidelberg (2007)"},{"key":"11_CR3","series-title":"LNCS","first-page":"97","volume-title":"European Conf. on Planning (ECP)","author":"A. Armando","year":"2000","unstructured":"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.\u00a01809, pp.\u00a097\u2013108. Springer, Heidelberg (2000)"},{"key":"11_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Intl. Workshop on Model Checking Software (SPIN)","author":"A. Armando","year":"2006","unstructured":"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.\u00a03925, pp.\u00a0146\u2013162. Springer, Heidelberg (2006)"},{"key":"11_CR5","series-title":"LNCS","first-page":"195","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, 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.\u00a02392, pp.\u00a0195\u2013210. Springer, Heidelberg (2002)"},{"key":"11_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"11_CR7","unstructured":"Babi\u0107, D.: Exploiting structure for scalable software verification. Ph.D. thesis, University of British Columbia (2008)"},{"key":"11_CR8","first-page":"203","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"T. Ball","year":"2001","unstructured":"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.\u00a0203\u2013213. ACM, New York (2001)"},{"key":"11_CR9","volume-title":"Intl. Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)","author":"C. Barrett","year":"2003","unstructured":"Barrett, C., Berezin, S.: A proof-producing Boolean search engine. In: Intl. Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) (2003)"},{"key":"11_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C. Barrett","year":"2011","unstructured":"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.\u00a06806, pp.\u00a0171\u2013177. Springer, Heidelberg (2011)"},{"key":"11_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"C. Barrett","year":"2006","unstructured":"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.\u00a04246, pp.\u00a0512\u2013526. Springer, Heidelberg (2006)"},{"key":"11_CR12","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2009","unstructured":"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.\u00a0185, pp.\u00a0825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"11_CR13","first-page":"21","volume":"3","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J.\u00a0Satisf. Boolean Model. Comput. 3, 21\u201346 (2007)","journal-title":"J.\u00a0Satisf. Boolean Model. Comput."},{"key":"11_CR14","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.smtlib.org"},{"key":"11_CR15","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"C. Barrett","year":"2010","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"key":"11_CR16","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Tech. rep., Department of Computer Science, University of Iowa (2010)"},{"key":"11_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0298\u2013302. Springer, Heidelberg (2007)"},{"key":"11_CR18","first-page":"522","volume-title":"Design Automation Conf. (DAC)","author":"C.W. Barrett","year":"1998","unstructured":"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.\u00a0522\u2013527. ACM, New York (1998)"},{"key":"11_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C.W. Barrett","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0236\u2013249 (2002)"},{"issue":"4","key":"11_CR20","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s10817-006-9026-1","volume":"35","author":"C.W. Barrett","year":"2005","unstructured":"Barrett, C.W., de Moura, L., Stump, A.: Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). J.\u00a0Autom. Reason. 35(4), 373\u2013390 (2005)","journal-title":"J.\u00a0Autom. Reason."},{"key":"11_CR21","series-title":"LNCS","first-page":"521","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Berezin","year":"2003","unstructured":"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.\u00a02619, pp.\u00a0521\u2013536. Springer, Heidelberg (2003)"},{"key":"11_CR22","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"11_CR23","volume-title":"Handbook of Model Checking","author":"A. Biere","year":"2018","unstructured":"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)"},{"key":"11_CR24","series-title":"LNCS","first-page":"183","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"N. Bj\u00f8rner","year":"2007","unstructured":"Bj\u00f8rner, N., de Moura, L.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a04603, pp.\u00a0183\u2013198. Springer, Heidelberg (2007)"},{"key":"11_CR25","series-title":"LNCS","first-page":"376","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"N. Bj\u00f8rner","year":"1998","unstructured":"Bj\u00f8rner, 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.\u00a01384, pp.\u00a0376\u2013392. Springer, Heidelberg (1998)"},{"key":"11_CR26","first-page":"1","volume-title":"Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT\/BPR)","author":"F. Bobot","year":"2008","unstructured":"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.\u00a01\u20135. ACM, New York (2008)"},{"key":"11_CR27","first-page":"1","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M. Bofill","year":"2008","unstructured":"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.\u00a01\u20138. IEEE, Piscataway (2008)"},{"key":"11_CR28","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Intl. Conf. on Interactive Theorem Proving (ITP)","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, 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.\u00a06172, pp.\u00a0179\u2013194. Springer, Heidelberg (2010)"},{"key":"11_CR29","series-title":"LNCS","first-page":"151","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"T. Bouton","year":"2009","unstructured":"Bouton, T., De Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a05663, pp.\u00a0151\u2013156. Springer, Heidelberg (2009)"},{"key":"11_CR30","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Bozzano","year":"2005","unstructured":"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.\u00a03576. Springer, Heidelberg (2005)"},{"issue":"10","key":"11_CR31","doi-asserted-by":"crossref","first-page":"1411","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M. Bozzano","year":"2006","unstructured":"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\u20131596 (2006)","journal-title":"Inf. Comput."},{"key":"11_CR32","series-title":"LNCS","first-page":"317","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Bozzano","year":"2005","unstructured":"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.\u00a03440, pp.\u00a0317\u2013333 (2005)"},{"key":"11_CR33","series-title":"LNCS","first-page":"427","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"A. Bradley","year":"2006","unstructured":"Bradley, A., Manna, Z., Sipma, H.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a03855, pp.\u00a0427\u2013442. Springer, Heidelberg (2006)"},{"key":"11_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/978-3-642-35873-9_27","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"M. Brain","year":"2013","unstructured":"Brain, M., D\u2019Silva, 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.\u00a07737, pp.\u00a0455\u2013475. Springer, Heidelberg (2013)"},{"key":"11_CR35","first-page":"6","volume-title":"Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT\/BPR)","author":"R. Brummayer","year":"2008","unstructured":"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.\u00a06\u201311. ACM, New York (2008)"},{"key":"11_CR36","series-title":"LNCS","first-page":"174","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Brummayer","year":"2009","unstructured":"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.\u00a05505, pp.\u00a0174\u2013177. Springer, Heidelberg (2009)"},{"key":"11_CR37","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, 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.\u00a04590, pp.\u00a0547\u2013560. Springer, Heidelberg (2007)"},{"issue":"1\u20132","key":"11_CR38","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10472-009-9152-7","volume":"55","author":"R. Bruttomesso","year":"2009","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1\u20132), 63\u201399 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"11_CR39","series-title":"LNCS","first-page":"150","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Bruttomesso","year":"2010","unstructured":"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.\u00a06015, pp.\u00a0150\u2013153. Springer, Heidelberg (2010)"},{"key":"11_CR40","first-page":"770","volume-title":"Intl. Conf. on Computer-Aided Design","author":"R. Bruttomesso","year":"2010","unstructured":"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.\u00a0770\u2013777. IEEE, Piscataway (2010)"},{"key":"11_CR41","first-page":"13","volume-title":"Intl. Conf. on Computer-Aided Design","author":"R. Bruttomesso","year":"2009","unstructured":"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.\u00a013\u201320. ACM, New York (2009)"},{"key":"11_CR42","series-title":"LNCS","first-page":"106","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bryant","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0106\u2013122. Springer, Heidelberg (2002)"},{"key":"11_CR43","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R.E. Bryant","year":"1999","unstructured":"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.\u00a01633, pp.\u00a0470\u2013482. Springer, Heidelberg (1999)"},{"key":"11_CR44","series-title":"LNCS","first-page":"358","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R.E. Bryant","year":"2007","unstructured":"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.\u00a04424, pp.\u00a0358\u2013372. Springer, Heidelberg (2007)"},{"key":"11_CR45","volume-title":"Intl. Workshop on Constraints in Formal Verification (CFV)","author":"R.E. Bryant","year":"2002","unstructured":"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)"},{"issue":"4","key":"11_CR46","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1145\/566385.566390","volume":"3","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4), 604\u2013627 (2002)","journal-title":"ACM Trans. Comput. Log."},{"key":"11_CR47","series-title":"LNCS","first-page":"492","volume-title":"Automated Deduction in Classical and Non-classical Logics","author":"D. Cantone","year":"2000","unstructured":"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.\u00a01761, pp.\u00a0492\u2013495. Springer, Heidelberg (2000)"},{"key":"11_CR48","volume-title":"Handbook of Model Checking","author":"S. Chaki","year":"2018","unstructured":"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)"},{"key":"11_CR49","series-title":"LNCS","first-page":"19","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S., Qadeer, S., Rakamari\u0107, 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.\u00a04424, pp.\u00a019\u201333. Springer, Heidelberg (2007)"},{"key":"11_CR50","series-title":"LNCS","first-page":"349","volume-title":"Annual European Symp. on Algorithms (ESA)","author":"B.V. Cherkassy","year":"1996","unstructured":"Cherkassy, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: D\u00edaz, J., Serna, M.J. (eds.) Annual European Symp. on Algorithms (ESA). LNCS, vol.\u00a01136, pp.\u00a0349\u2013363. Springer, Heidelberg (1996)"},{"key":"11_CR51","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Intl. Workshop on Model Checking Software (SPIN)","author":"J. Christ","year":"2012","unstructured":"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.\u00a07385, pp.\u00a0248\u2013254. Springer, Heidelberg (2012)"},{"key":"11_CR52","series-title":"LNCS","first-page":"124","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"J. Christ","year":"2013","unstructured":"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.\u00a07795, pp.\u00a0124\u2013138. Springer, Heidelberg (2013)"},{"key":"11_CR53","series-title":"LNCS","first-page":"93","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Cimatti","year":"2013","unstructured":"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.\u00a07795, pp.\u00a093\u2013107. Springer, Heidelberg (2013)"},{"key":"11_CR54","series-title":"LNCS","first-page":"397","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Cimatti","year":"2008","unstructured":"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.\u00a04963, pp.\u00a0397\u2013412. Springer, Berlin (2008)"},{"issue":"1","key":"11_CR55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 1\u201354 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"11_CR56","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1613\/jair.3196","volume":"40","author":"A. Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J.\u00a0Artif. Intell. Res. 40(1), 701\u2013728 (2011)","journal-title":"J.\u00a0Artif. Intell. Res."},{"issue":"1","key":"11_CR57","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"11_CR58","series-title":"LNCS","first-page":"170","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"S. Cotton","year":"2006","unstructured":"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.\u00a04121, pp.\u00a0170\u2013183. Springer, Heidelberg (2006)"},{"key":"11_CR59","unstructured":"Cotton, S., Maler, O.: Satisfiability modulo theory chains with DPLL(T). Tech. rep., Verimag (2006)"},{"issue":"3","key":"11_CR60","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J.\u00a0Symb. Log. 22(3), 269\u2013285 (1957)","journal-title":"J.\u00a0Symb. Log."},{"key":"11_CR61","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Cyrluk","year":"1997","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, 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.\u00a01254, pp.\u00a060\u201371. Springer, Heidelberg (1997)"},{"issue":"7","key":"11_CR62","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"11_CR63","first-page":"201","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J.\u00a0ACM 7(3), 201\u2013215 (1960)","journal-title":"J.\u00a0ACM"},{"issue":"3","key":"11_CR64","first-page":"365","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J.\u00a0ACM 52(3), 365\u2013473 (2005)","journal-title":"J.\u00a0ACM"},{"key":"11_CR65","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"I. Dillig","year":"2009","unstructured":"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.\u00a05643, pp.\u00a0233\u2013247. Springer, Heidelberg (2009)"},{"issue":"4","key":"11_CR66","first-page":"758","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J.\u00a0ACM 27(4), 758\u2013771 (1980)","journal-title":"J.\u00a0ACM"},{"key":"11_CR67","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"B. Dutertre","year":"2006","unstructured":"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.\u00a04144, pp.\u00a081\u201394. Springer, Heidelberg (2006)"},{"key":"11_CR68","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. rep., CSL, SRI International (2006)"},{"key":"11_CR69","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Tech. rep., SRI International (2006)"},{"issue":"3","key":"11_CR70","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10817-010-9200-3","volume":"48","author":"Mnacho Echenim","year":"2010","unstructured":"Echenim, M., Peltier, N.: An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 293\u2013362 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR71","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Cambridge (2001)","edition":"2"},{"key":"11_CR72","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C. Flanagan","year":"2003","unstructured":"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.\u00a02725, pp.\u00a0355\u2013367. Springer, Heidelberg (2003)"},{"key":"11_CR73","series-title":"LNCS","first-page":"167","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Fontaine","year":"2006","unstructured":"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.\u00a03920, pp.\u00a0167\u2013181. Springer, Berlin (2006)"},{"key":"11_CR74","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-642-38536-0_33","volume-title":"Computer Science: Theory and Applications","author":"A. Fr\u00f6hlich","year":"2013","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, 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.\u00a07913, pp.\u00a0378\u2013390. Springer, Heidelberg (2013)"},{"key":"11_CR75","series-title":"LNCS","first-page":"413","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Fuchs","year":"2009","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krsti\u0107, 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.\u00a05505, pp.\u00a0413\u2013427. Springer, Heidelberg (2009)"},{"key":"11_CR76","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"V. Ganesh","year":"2007","unstructured":"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.\u00a04590, pp.\u00a0519\u2013531. Springer, Heidelberg (2007)"},{"key":"11_CR77","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"H. Ganzinger","year":"2004","unstructured":"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.\u00a03114, pp.\u00a0175\u2013188. Springer, Heidelberg (2004)"},{"key":"11_CR78","first-page":"55","volume-title":"Symp. on Logic in Computer Science","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Symp. on Logic in Computer Science, vol.\u00a0LICS, pp.\u00a055\u201364. IEEE, Piscataway (2003)"},{"key":"11_CR79","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"H. Ganzinger","year":"2006","unstructured":"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.\u00a04246, pp.\u00a0497\u2013511. Springer, Heidelberg (2006)"},{"key":"11_CR80","series-title":"LNCS","first-page":"208","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"S. Gao","year":"2013","unstructured":"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.\u00a07898, pp.\u00a0208\u2013214. Springer, Berlin (2013)"},{"key":"11_CR81","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"Y. Ge","year":"2008","unstructured":"Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2008)"},{"key":"11_CR82","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"Y. Ge","year":"2007","unstructured":"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.\u00a04603, pp.\u00a0167\u2013182. Springer, Heidelberg (2007)"},{"key":"11_CR83","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"Y. Ge","year":"2009","unstructured":"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.\u00a05643, pp.\u00a0306\u2013320. Springer, Heidelberg (2009)"},{"issue":"3\u20134","key":"11_CR84","first-page":"221","volume":"33","author":"S. Ghilardi","year":"2005","unstructured":"Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J.\u00a0Autom. Reason. 33(3\u20134), 221\u2013249 (2005)","journal-title":"J.\u00a0Autom. Reason."},{"key":"11_CR85","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/978-3-540-73595-3_25","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"S. Ghilardi","year":"2007","unstructured":"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.\u00a04603, pp.\u00a0362\u2013378. Springer, Heidelberg (2007)"},{"key":"11_CR86","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"S. Ghilardi","year":"2008","unstructured":"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.\u00a05195, pp.\u00a067\u201382. Springer, Heidelberg (2008)"},{"issue":"2","key":"11_CR87","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1342991.1342992","volume":"9","author":"S. Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 1\u201354 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"11_CR88","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"S. Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol.\u00a06173, pp.\u00a022\u201329. Springer, Heidelberg (2010)"},{"key":"11_CR89","first-page":"12","volume-title":"Joint Workshops of the Intl. Workshop on Satisfiability Modulo Theories and the Intl. Workshop on Bit-Precise Reasoning (SMT\/BPR)","author":"A. Goel","year":"2008","unstructured":"Goel, A., Krsti\u0107, 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.\u00a012\u201317. ACM, New York (2008)"},{"key":"11_CR90","series-title":"LNCS","first-page":"183","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"A. Goel","year":"2009","unstructured":"Goel, A., Krsti\u0107, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a05663, pp.\u00a0183\u2013198. Springer, Heidelberg (2009)"},{"key":"11_CR91","unstructured":"Griggio, A.: An effective SMT engine for formal verification. Ph.D. thesis, DISI, University of Trento (2009)"},{"key":"11_CR92","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"A. Griggio","year":"2010","unstructured":"Griggio, A.: A practical approach to SMT(LA(Z)). In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"key":"11_CR93","first-page":"109","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"G. Hagen","year":"2008","unstructured":"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.\u00a0109\u2013117. IEEE, Piscataway (2008)"},{"key":"11_CR94","unstructured":"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"},{"key":"11_CR95","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Jhala","year":"2005","unstructured":"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.\u00a03576, pp.\u00a039\u201351. Springer, Heidelberg (2005)"},{"key":"11_CR96","volume-title":"Handbook of Model Checking","author":"R. Jhala","year":"2018","unstructured":"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)"},{"key":"11_CR97","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"D. Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol.\u00a06397, pp.\u00a0402\u2013416. Springer, Heidelberg (2010)"},{"key":"11_CR98","first-page":"173","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"D. Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, 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.\u00a0173\u2013180. IEEE, Piscataway (2013)"},{"key":"11_CR99","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"D. Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, 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.\u00a07364, pp.\u00a0339\u2013354. Springer, Heidelberg (2012)"},{"key":"11_CR100","first-page":"105","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"D. Kapur","year":"2006","unstructured":"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.\u00a0105\u2013116. ACM, New York (2006)"},{"key":"11_CR101","unstructured":"Kapur, D., Zarba, C.G.: A reduction approach to decision procedures. Tech. rep., University of New Mexico (2005)"},{"key":"11_CR102","first-page":"105","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"A. Kiezun","year":"2009","unstructured":"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.\u00a0105\u2013116. ACM, New York (2009)"},{"key":"11_CR103","first-page":"31","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"H. Kim","year":"2006","unstructured":"Kim, H., Somenzi, F.: Finite instantiations for integer difference logic. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a031\u201338. IEEE, Piscataway (2006)"},{"key":"11_CR104","first-page":"189","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"T. King","year":"2013","unstructured":"King, T., Barrett, C., Dutertre, B.: Sum of infeasibility simplex for SMT. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0189\u2013196. IEEE, Piscataway (2013)"},{"key":"11_CR105","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver\u2014an 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.\u00a05195, pp.\u00a0292\u2013298. Springer, Heidelberg (2008)"},{"key":"11_CR106","series-title":"LNCS","first-page":"509","volume-title":"Intl. Conf. on Principles and Practice of Constraint Programming (CP)","author":"K. Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol.\u00a05732, pp.\u00a0509\u2013523. Springer, Heidelberg (2009)"},{"key":"11_CR107","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"11_CR108","series-title":"LNCS","first-page":"1","volume-title":"Intl. Symp. on Frontiers of Combining Systems (FroCoS)","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, 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.\u00a04720, pp.\u00a01\u201327. Springer, Heidelberg (2007)"},{"key":"11_CR109","series-title":"LNCS","first-page":"618","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, 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.\u00a04424, pp.\u00a0618\u2013631. Springer, Heidelberg (2007)"},{"key":"11_CR110","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M., O\u2019Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a02517, pp.\u00a0142\u2013159. Springer, Heidelberg (2002)"},{"key":"11_CR111","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"T. Lev-Ami","year":"2005","unstructured":"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.\u00a03632, pp.\u00a099\u2013115. Springer, Heidelberg (2005)"},{"key":"11_CR112","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"Formal Methods at the Crossroads: From Panacea to Foundational Support","author":"Z. Manna","year":"2003","unstructured":"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.\u00a02757, pp.\u00a0381\u2013422. Springer, Heidelberg (2003)"},{"key":"11_CR113","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-540-73368-3_35","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Manolios","year":"2007","unstructured":"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.\u00a04590, pp.\u00a0303\u2013306. Springer, Heidelberg (2007)"},{"key":"11_CR114","first-page":"3","volume-title":"Many-Sorted Logic and Its Applications","author":"M. Manzano","year":"1993","unstructured":"Manzano, M.: Introduction to many-sorted logic. In: Meinke, K., Tucker, J.V. (eds.) Many-Sorted Logic and Its Applications, pp.\u00a03\u201386. Wiley, New York (1993)"},{"key":"11_CR115","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K. McMillan","year":"2003","unstructured":"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.\u00a02725, pp.\u00a01\u201313. Springer, Heidelberg (2003)"},{"key":"11_CR116","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K.L. McMillan","year":"2005","unstructured":"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.\u00a03440, pp.\u00a01\u201312. Springer, Heidelberg (2005)"},{"issue":"1","key":"11_CR117","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR118","volume-title":"Handbook of Model Checking","author":"K.L. McMillan","year":"2018","unstructured":"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)"},{"key":"11_CR119","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"2009","unstructured":"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.\u00a05643, pp.\u00a0462\u2013476 (2009)"},{"key":"11_CR120","series-title":"LNCS","first-page":"486","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Moskal","year":"2008","unstructured":"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.\u00a04963, pp.\u00a0486\u2013500. Springer, Heidelberg (2008)"},{"key":"11_CR121","first-page":"337","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, 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.\u00a04963, pp.\u00a0337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR122","first-page":"45","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"L. Moura de","year":"2009","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a045\u201352. IEEE, Piscataway (2009)"},{"key":"11_CR123","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Model-based theory combination. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2007)"},{"key":"11_CR124","volume-title":"Intl. Symp. on the Theory and Applications of Satisfiability Testing (SAT)","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Intl. Symp. on the Theory and Applications of Satisfiability Testing (SAT) (2002)"},{"key":"11_CR125","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, 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.\u00a02725, pp.\u00a014\u201326. Springer, Heidelberg (2003)"},{"issue":"2","key":"11_CR126","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"2","key":"11_CR127","first-page":"356","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J.\u00a0ACM 27(2), 356\u2013364 (1980)","journal-title":"J.\u00a0ACM"},{"key":"11_CR128","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Nieuwenhuis","year":"2005","unstructured":"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.\u00a03576, pp.\u00a0321\u2013334. Springer, Heidelberg (2005)"},{"key":"11_CR129","series-title":"LNCS","first-page":"156","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"R. Nieuwenhuis","year":"2006","unstructured":"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.\u00a04121, pp.\u00a0156\u2013169. Springer, Heidelberg (2006)"},{"issue":"4","key":"11_CR130","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R. Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"11_CR131","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"R. Nieuwenhuis","year":"2005","unstructured":"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.\u00a03452, pp.\u00a036\u201350. Springer, Heidelberg (2005)"},{"issue":"6","key":"11_CR132","first-page":"937","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J.\u00a0ACM 53(6), 937\u2013977 (2006)","journal-title":"J.\u00a0ACM"},{"key":"11_CR133","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"D. Oe","year":"2009","unstructured":"Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2009)"},{"key":"11_CR134","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR135","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods Symp. (NFM)","author":"J. Peleska","year":"2011","unstructured":"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.\u00a06617, pp.\u00a0298\u2013312. Springer, Heidelberg (2011)"},{"key":"11_CR136","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"R. Piskac","year":"2008","unstructured":"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.\u00a04905, pp.\u00a0218\u2013232. Springer, Heidelberg (2008)"},{"key":"11_CR137","series-title":"LNCS","first-page":"687","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Pnueli","year":"1999","unstructured":"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.\u00a01633, pp.\u00a0687\u2013688. Springer, Heidelberg (1999)"},{"key":"11_CR138","first-page":"92","volume-title":"Comptes Rendus du I Congr\u00e8s de Math\u00e9maticiens des Pays Slaves","author":"M. Presburger","year":"1929","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I Congr\u00e8s de Math\u00e9maticiens des Pays Slaves, Warsaw, pp.\u00a092\u2013101 (1929)"},{"issue":"3","key":"11_CR139","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J.\u00a0Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J.\u00a0Symb. Log."},{"key":"11_CR140","first-page":"4","volume-title":"Conf. on Supercomputing (SC)","author":"W. Pugh","year":"1991","unstructured":"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.\u00a04\u201313. IEEE\/ACM, Piscataway\/New York (1991)"},{"key":"11_CR141","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Intl. Symp. on Frontiers of Combining Systems (FroCoS)","author":"S. Ranise","year":"2005","unstructured":"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.\u00a03717, pp.\u00a048\u201364. Springer, Heidelberg (2005)"},{"key":"11_CR142","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a08044, pp.\u00a0640\u2013655. Springer, Heidelberg (2013)"},{"key":"11_CR143","series-title":"LNCS","first-page":"377","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"A. Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a07898, pp.\u00a0377\u2013391. Springer, Heidelberg (2013)"},{"key":"11_CR144","volume-title":"Intl. Workshop on Satisfiability Modulo Theories (SMT)","author":"P. R\u00fcmmer","year":"2010","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: Intl. Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"key":"11_CR145","doi-asserted-by":"crossref","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A. Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J.\u00a0Symb. Comput. 45, 1212\u20131233 (2010)","journal-title":"J.\u00a0Symb. Comput."},{"key":"11_CR146","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)"},{"issue":"3\u20134","key":"11_CR147","first-page":"141","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J.\u00a0Satisf. Boolean Model. Comput. 3(3\u20134), 141\u2013224 (2007)","journal-title":"J.\u00a0Satisf. Boolean Model. Comput."},{"key":"11_CR148","series-title":"LNCS","first-page":"108","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, 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.\u00a01954, pp.\u00a0108\u2013125. Springer, Heidelberg (2000)"},{"key":"11_CR149","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/11499107_18","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"H.M. Sheini","year":"2005","unstructured":"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.\u00a03569, pp.\u00a0241\u2013256. Springer, Heidelberg (2005)"},{"key":"11_CR150","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a03632, pp.\u00a0219\u2013234. Springer, Heidelberg (2005)"},{"key":"11_CR151","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-36126-X_10","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"O. Strichman","year":"2002","unstructured":"Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Aagaard, M., O\u2019Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a02517, pp.\u00a0160\u2013170. Springer, Heidelberg (2002)"},{"key":"11_CR152","series-title":"LNCS","first-page":"113","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"O. Strichman","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0113\u2013124. Springer, Heidelberg (2002)"},{"key":"11_CR153","first-page":"29","volume-title":"Symp. on Logic in Computer Science","author":"A. Stump","year":"2001","unstructured":"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.\u00a0LICS, pp.\u00a029\u201337. IEEE, Piscataway (2001)"},{"issue":"1","key":"11_CR154","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"41","author":"A. Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Form. Methods Syst. Des. 41(1), 91\u2013118 (2013)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"11_CR155","first-page":"215","volume":"22","author":"R.E. Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J.\u00a0ACM 22(2), 215\u2013225 (1975)","journal-title":"J.\u00a0ACM"},{"key":"11_CR156","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/3-540-45757-7_26","volume-title":"European Conf. on Logics in Artificial Intelligence (JELIA)","author":"C. Tinelli","year":"2002","unstructured":"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.\u00a02424, pp.\u00a0308\u2013319. Springer, Heidelberg (2002)"},{"key":"11_CR157","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Intl. Workshop on Frontiers of Combining Systems (FroCoS)","author":"C. Tinelli","year":"1996","unstructured":"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.\u00a0103\u2013120. Kluwer Academic, Dordrecht (1996)"},{"issue":"1","key":"11_CR158","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR159","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"European Conf. on Logics in Artificial Intelligence (JELIA)","author":"C. Tinelli","year":"2004","unstructured":"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.\u00a03229, pp.\u00a0641\u2013653. Springer, Heidelberg (2004)"},{"issue":"3","key":"11_CR160","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.: Combining nonstably infinite theories. J.\u00a0Autom. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J.\u00a0Autom. Reason."},{"key":"11_CR161","first-page":"235","volume-title":"Design Automation Conf. (DAC)","author":"C. Wang","year":"2006","unstructured":"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.\u00a0235\u2013240. ACM, New York (2006)"},{"key":"11_CR162","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a03632, pp.\u00a0353\u2013368. Springer, Heidelberg (2005)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T05:44:41Z","timestamp":1571377481000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":162,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}