{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:10:20Z","timestamp":1760015420003},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661667"},{"type":"electronic","value":"9783319661674"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_2","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:15:18Z","timestamp":1503918918000},"page":"22-40","source":"Crossref","is-referenced-by-count":12,"title":["Designing Theory Solvers with Extensions"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-21690-4_29","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: an SMT solver for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462\u2013469. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21690-4_29"},{"issue":"3","key":"2_CR2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: Metitarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"2_CR3","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s10817-015-9356-y","volume":"56","author":"J Avigad","year":"2016","unstructured":"Avigad, J., Lewis, R.Y., Roux, C.: A heuristic prover for real inequalities. J. Autom. Reason. 56(3), 367\u2013386 (2016)","journal-title":"J. Autom. Reason."},{"key":"2_CR4","unstructured":"Ball, T., Daniel, J.: Deconstructing dynamic symbolic execution. In: Proceedings of the 2014 Marktoberdorf Summer School on Dependable Software Systems Engineering. IOS Press (2014)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-40229-1_7","volume-title":"Automated Reasoning","author":"K Bansal","year":"2016","unstructured":"Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 82\u201398. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40229-1_7"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-21668-3_6","volume-title":"Computer Aided Verification","author":"K Bansal","year":"2015","unstructured":"Bansal, K., Reynolds, A., King, T., Barrett, C., Wies, T.: Deciding local theory extensions via e-matching. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 87\u2013105. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21668-3_6"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_14"},{"key":"2_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). \nwww.SMT-LIB.org"},{"key":"2_CR9","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). \nwww.SMT-LIB.org"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","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.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). doi:\n10.1007\/11916277_35"},{"key":"2_CR11","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, Chap. 26, vol. 185, pp. 825\u2013885. IOS Press, February 2009"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307\u2013321. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-00768-2_27"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45, 213 (2014)","journal-title":"Form. Methods Syst. Des."},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-00768-2_16"},{"key":"2_CR15","first-page":"165","volume":"6","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput. 6, 165\u2013201 (2009)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., et al.: A lazy and layered SMT(\n            $$\\cal{BV}$$\n          ) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 547\u2013560. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-73368-3_54"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-662-54577-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2017","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58\u201375. Springer, Heidelberg (2017). doi:\n10.1007\/978-3-662-54577-5_4"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45069-6_39"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-78800-3_24"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura","year":"2013","unstructured":"Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-35873-9_1"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_49"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). doi:\n10.1007\/11817963_11"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340\u2013354. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-72788-0_33"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39611-3_21"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184\u2013191. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08587-6_13"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","volume-title":"Computer Aided Verification","author":"L Hadarean","year":"2014","unstructured":"Hadarean, L., Bansal, K., Jovanovi\u0107, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680\u2013695. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_45"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-52234-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Jovanovi\u0107","year":"2017","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330\u2013346. Springer, Cham (2017). doi:\n10.1007\/978-3-319-52234-0_18"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-31365-3_27"},{"key":"2_CR29","unstructured":"King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, Courant Institute of Mathematical Sciences New York (2014)"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-54862-8_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Leike","year":"2014","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54862-8_12"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_43"},{"issue":"6","key":"2_CR32","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","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. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-21401-6_13","volume-title":"Automated Deduction \u2013 CADE-25","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 197\u2013213. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21401-6_13"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). doi:\n10.1007\/978-3-319-63390-9_24"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005). doi:\n10.1007\/11532231_16"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: Yung, M., Li, N. (eds.) Proceedings of the 21st ACM Conference on Computer and Communications Security (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"2_CR37","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.entcs.2012.11.004","volume":"289","author":"T Khanh Van","year":"2012","unstructured":"Van Khanh, T., Ogawa, M.: SMT for polynomial constraints on real numbers. Electron. Notes Theor. Comput. Sci. 289, 27\u201340 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-40970-2_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"A Zelji\u0107","year":"2016","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249\u2013266. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40970-2_16"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a z3-based string solver for web application analysis. In: Foundations of Software Engineering, ESEC\/FSE 2013 (2013)","DOI":"10.1145\/2491411.2491456"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:16:12Z","timestamp":1503918972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}