{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:27:24Z","timestamp":1740547644013,"version":"3.38.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,9,4]],"date-time":"2010-09-04T00:00:00Z","timestamp":1283558400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,1]]},"DOI":"10.1007\/s10817-010-9196-8","type":"journal-article","created":{"date-parts":[[2010,9,3]],"date-time":"2010-09-03T09:31:01Z","timestamp":1283506261000},"page":"107-131","source":"Crossref","is-referenced-by-count":31,"title":["SAT Modulo Linear Arithmetic for Solving Polynomial Constraints"],"prefix":"10.1007","volume":"48","author":[{"given":"Cristina","family":"Borralleras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,9,4]]},"reference":[{"key":"9196_CR1","doi-asserted-by":"crossref","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST\u201910 (2010)","DOI":"10.1007\/978-3-642-17796-5_12"},{"key":"9196_CR2","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: The Satisfiability Modulo Theories Competition (SMT-COMP). http:\/\/www.smtcomp.org (2009)"},{"key":"9196_CR3","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.smt-lib.org (2008)"},{"key":"9196_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Proceedings of the 19th International Conference on Computer Aided Verification, CAV\u201907. Lecture Notes in Computer Science, vol. 4590, pp. 298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"9196_CR5","doi-asserted-by":"crossref","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer (2003)","DOI":"10.1007\/978-3-662-05355-3"},{"key":"9196_CR6","doi-asserted-by":"crossref","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The Barcelogic SMT solver. In: Proceedings of the 20th International Conference on Computer Aided Verification, CAV\u201908. Lecture Notes in Computer Science, vol. 5123, pp. 294\u2013298. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"9196_CR7","doi-asserted-by":"crossref","unstructured":"Borralleras, C., Lucas, S., Navarro-Marset, R., Rodr\u00edguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Proceedings of the 22nd International Conference on Automated Deduction, CADE-22. Lecture Notes in Computer Science, vol. 5663, pp. 294\u2013305. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_23"},{"key":"9196_CR8","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of 15th International Conference on Computer Aided Verification, CAV\u201903. Lecture Notes in Computer Science, vol. 2725, pp. 420\u2013432. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"issue":"4","key":"9196_CR9","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E Contejean","year":"2006","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J Autom Reason 34(4), 325\u2013363. Springer (2006)","journal-title":"J Autom Reason"},{"key":"9196_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL\u201978, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"9196_CR11","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f6rner, N.: Z3: An efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9196_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L., Olney Passmore, G.: On Locally Minimal Nullstellensatz Proofs. Technical Report, Microsoft Research, MSR-TR-2009-90.pdf (2009)","DOI":"10.1145\/1670412.1670418"},{"key":"9196_CR13","unstructured":"Doltzmann, A., Sturm, T.: REDLOG: Computer Algebra Meets Computer Logic. Technical Report, University of Passau, MIP-9603 (1996)"},{"key":"9196_CR14","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of the 18th International Conference on Computer Aided Verification, CAV\u201906. Lecture Notes in Computer Science, vol. 4144, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"issue":"3\u20134","key":"9196_CR15","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3\u20134), 209\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9196_CR16","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201907. Lecture Notes in Computer Science, vol. 4501, pp. 340\u2013354. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"9196_CR17","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: Proceedings of the 9th International Conference on Intelligent Computer Mathematics, AISC\u201908. Lecture Notes in Computer Science, vol. 5144, pp. 109\u2013124. Springer (2008)","DOI":"10.1007\/978-3-540-85110-3_10"},{"key":"9196_CR18","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ivanc\u0306i\u0107, F.: Efficient decision procedure for non-linear arithmetic constraints using CORDIC. In: Proceedings of the 9th International Conference on Formal Methods in Computer Aided Design, FMCAD\u201909, pp. 61\u201368. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351140"},{"key":"9196_CR19","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco (1979)"},{"key":"9196_CR20","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating polynomial orderings for termination proofs. In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications, RTA\u201995. Lecture Notes in Computer Science, vol. 914, pp. 426\u2013431. Springer (1995)","DOI":"10.1007\/3-540-59200-8_77"},{"key":"9196_CR21","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: Automatic termination proofs in the dependency pair framework. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning, IJCAR\u201906. Lecture Notes in Computer Science, vol. 4130, pp. 281\u2013286. Springer (2006)","DOI":"10.1007\/11814771_24"},{"key":"9196_CR22","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/1375581.1375616","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, PLDI\u201908","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, PLDI\u201908, pp. 281\u2013292. ACM Press, New York (2008)"},{"issue":"4","key":"9196_CR23","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1016\/j.ipl.2005.12.011","volume":"98","author":"D Hofbauer","year":"2006","unstructured":"Hofbauer, D., Waldmann, J.: Termination of {aa \u2192 bc, bb \u2192 ac, cc \u2192 ab}. Inf. Process. Lett. 98(4), 156\u2013158 (2006)","journal-title":"Inf. Process. Lett."},{"key":"9196_CR24","unstructured":"Hong, H., et al.: http:\/\/www.usna.edu\/Users\/cs\/qepcad\/B\/WhatisQEPCAD.html . Accessed June 2010"},{"key":"9196_CR25","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proceedings of the IMACS International Conference on Applications of Computer Algebra (2004)"},{"key":"9196_CR26","doi-asserted-by":"crossref","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and Control, HSCC\u201999. Lecture Notes in Computer Science, vol. 1569, pp. 137\u2013151. Springer (1999)","DOI":"10.1007\/3-540-48983-5_15"},{"key":"9196_CR27","unstructured":"Lucas, S.: MU-TERM: a tool for proving termination of context-sensitive rewriting. In: Proceedings of the 15th International Conference on Rewriting Techniques and Applications, RTA\u201904. Lecture Notes in Computer Science, vol. 3091, pp. 200\u2013209. Springer (2004). http:\/\/zenon.dsic.upv.es\/muterm . Accessed June 2010"},{"issue":"3","key":"9196_CR28","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO ITA 39(3), 547\u2013586 (2005)","journal-title":"RAIRO ITA"},{"key":"9196_CR29","first-page":"39","volume-title":"Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP\u201907","author":"S Lucas","year":"2007","unstructured":"Lucas, S.: Practical use of polynomials over the reals in proofs of termination. In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP\u201907, pp. 39\u201350. ACM Press, New York (2007)"},{"key":"9196_CR30","doi-asserted-by":"crossref","unstructured":"Nguyen, M.T., De Schreye, D.: Polynomial interpretations as a basis for termination analysis of logic programs. In: Proceedings of the 21st International Conference on Logic Programming, ICLP\u201905. Lecture Notes in Computer Science, vol. 3668, pp. 311\u2013325. Springer (2005)","DOI":"10.1007\/11562931_24"},{"issue":"2","key":"9196_CR31","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"key":"9196_CR32","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Proceedings of the 11th International Symposium on Static Analysis, SAS\u201904. Lecture Notes in Computer Science, vol. 3148, pp. 53\u201368 (2004)","DOI":"10.1007\/978-3-540-27864-1_7"},{"issue":"1","key":"9196_CR33","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods in Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Form. Methods in Syst. Des."},{"key":"9196_CR34","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1145\/964001.964028","volume-title":"Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL\u201904","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL\u201904, pp. 318\u2013329. ACM Press, New York (2004)"},{"key":"9196_CR35","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, ASE\u201903, pp. 94\u2013105. IEEE Computer Society (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"issue":"2","key":"9196_CR36","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BF01362149","volume":"207","author":"G Stengle","year":"1973","unstructured":"Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87\u201397 (1973)","journal-title":"Math. Ann."},{"key":"9196_CR37","doi-asserted-by":"crossref","unstructured":"Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Proceedings of the 19th International Workshop on Computer Science Logic, CSL\u201905. Lecture Notes in Computer Science, vol. 3634, pp. 248\u2013262 (2005)","DOI":"10.1007\/11538363_18"},{"key":"9196_CR38","doi-asserted-by":"crossref","unstructured":"Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-16 (2010)","DOI":"10.1007\/978-3-642-17511-4_27"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9196-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9196-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9196-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T13:58:25Z","timestamp":1740491905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9196-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,4]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["9196"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9196-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2010,9,4]]}}}