{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:43:53Z","timestamp":1777347833661,"version":"3.51.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","type":"electronic"}],"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-52234-0_18","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"330-346","source":"Crossref","is-referenced-by-count":25,"title":["Solving Nonlinear Integer Arithmetic with MCSAT"],"prefix":"10.1007","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"18_CR1","volume-title":"Computer Algebra: Symbolic and Algebraic Computation","author":"R Albrecht","year":"2012","unstructured":"Albrecht, R., Buchberger, B., Collins, G.E., Loos, R.: Computer Algebra: Symbolic and Algebraic Computation, vol. 4. Springer, Vienna (2012)"},{"key":"18_CR2","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: 10.1007\/978-3-642-22110-1_14"},{"key":"18_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB), vol. 15, pp. 18\u201352 (2010). www.SMT-LIB.org"},{"key":"18_CR4","first-page":"825","volume":"185","author":"CW Barrett","year":"2009","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisf. 185, 825\u2013885 (2009)","journal-title":"Handb. Satisf."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20\u201323 May, pp. 134\u2013183 (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_26"},{"key":"18_CR7","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 de","year":"2008","unstructured":"de 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: 10.1007\/978-3-540-78800-3_24"},{"key":"18_CR8","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: 10.1007\/978-3-642-35873-9_1"},{"key":"18_CR9","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 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-08867-9_49"},{"key":"18_CR10","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: 10.1007\/11817963_11"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24605-3_37"},{"key":"18_CR12","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: 10.1007\/978-3-540-72788-0_33"},{"key":"18_CR13","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., et al.: 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, Heidelberg (2014). doi: 10.1007\/978-3-319-08587-6_13"},{"issue":"5","key":"18_CR14","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1090\/S0002-9904-1958-10224-4","volume":"64","author":"RE Gomory","year":"1958","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275\u2013278 (1958)","journal-title":"Bull. Am. Math. Soc."},{"key":"18_CR15","first-page":"1","volume":"8","author":"A Griggio","year":"2012","unstructured":"Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. J. Satisf. Boolean Model. Comput. 8, 1\u201327 (2012)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_2"},{"key":"18_CR17","unstructured":"Jovanovi\u0107, D.: SMT beyond DPLL(T): a new approach to theory solvers and theory combination. Ph.D. thesis, Courant Institute of Mathematical Sciences, New York (2012)"},{"key":"18_CR18","doi-asserted-by":"crossref","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. 173\u2013180 (2013)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., De Moura, L.: Solving non-linear arithmetic. In: International Joint Conference on Automated Reasoning, pp. 339\u2013354 (2012)","DOI":"10.1007\/978-3-642-31365-3_27"},{"issue":"1","key":"18_CR20","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., De Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reason. 51(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reason."},{"key":"18_CR21","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":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-319-45641-6_21","volume-title":"Computer Algebra in Scientific Computing","author":"G Kremer","year":"2016","unstructured":"Kremer, G., Corzilius, F., \u00c1brah\u00e1m, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315\u2013335. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-45641-6_21"},{"key":"18_CR23","unstructured":"Leike, J., Heizmann, M.: Geometric series as nontermination arguments for linear lasso programs. In: 14th International Workshop on Termination, p. 55 (2014)"},{"key":"18_CR24","unstructured":"Lopes, N.P., Aksoy, L., Manquinho, V., Monteiro, J.: Optimally solving the MCM problem using pseudo-boolean satisfiability (2011)"},{"key":"18_CR25","volume-title":"Hilbert\u2019s Tenth Problem","author":"YV Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s Tenth Problem. The MIT Press, Cambridge (1993)"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"4","key":"18_CR27","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"key":"18_CR28","first-page":"135","volume":"4","author":"G Robinson","year":"1969","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. Mach. Intell. 4, 135\u2013150 (1969)","journal-title":"Mach. Intell."},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Technical report R-109, Rand Corporation (1951)","DOI":"10.1525\/9780520348097"},{"issue":"2","key":"18_CR30","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85\u2013101 (1997)","journal-title":"Appl. Algebra Eng. Commun. Comput."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T06:34:52Z","timestamp":1658385292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}