{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:38Z","timestamp":1759638698291,"version":"3.40.3"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030654733"},{"type":"electronic","value":"9783030654740"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-65474-0_5","type":"book-chapter","created":{"date-parts":[[2021,1,13]],"date-time":"2021-01-13T13:13:42Z","timestamp":1610543622000},"page":"89-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Termination of Polynomial Loops"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-3177","authenticated-orcid":false,"given":"Marcel","family":"Hark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,13]]},"reference":[{"issue":"3","key":"5_CR1","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s00165-012-0252-5","volume":"25","author":"D Babi\u0107","year":"2013","unstructured":"Babi\u0107, D., Cook, B., Hu, A.J., Rakamaric, Z.: Proving termination of nonlinear command sequences. Formal Aspects Comput. 25(3), 389\u2013403 (2013). https:\/\/doi.org\/10.1007\/s00165-012-0252-5","journal-title":"Formal Aspects Comput."},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry, Algorithms and Computation in Mathematics","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, Algorithms and Computation in Mathematics, vol. 10. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/3-540-33099-2"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Basu, S., Mishra, B.: Computational and quantitative real algebraic geometry. In: Goodman, J.E., O\u2019Rourke, J., T\u00f3th, C.D. (eds.) Handbook of Discrete and Computational Geometry, 3rd edn. Chapman and Hall\/CRC, pp. 969\u20131002 (2017). https:\/\/doi.org\/10.1201\/9781315119601","DOI":"10.1201\/9781315119601"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/978-3-319-63390-9_32","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2017","unstructured":"Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 601\u2013620. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-030-32304-2_22","volume-title":"Static Analysis","author":"AM Ben-Amram","year":"2019","unstructured":"Ben-Amram, A.M., Dom\u00e9nech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 459\u2013480. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_22"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Deciding conditional termination. Logical Meth. Comput. Sci. 10(3) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(3:8)2014","DOI":"10.2168\/LMCS-10(3:8)2014"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113\u2013129. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_8"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M Braverman","year":"2006","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372\u2013385. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_34"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413\u2013429. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_28"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-Y Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156\u2013171. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_11"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"22","author":"PJ Cohen","year":"1969","unstructured":"Cohen, P.J.: Decision procedures for real and p-adic fields. Commun. Pure Appl. Math. 22(2), 131\u2013151 (1969). https:\/\/doi.org\/10.1002\/cpa.3160220202","journal-title":"Commun. Pure Appl. Math."},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-32943-2_5","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"L Dai","year":"2012","unstructured":"Dai, L., Xia, B.: Non-termination sets of simple linear loops. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 61\u201373. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32943-2_5"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0024-3795(95)00095-X","volume":"247","author":"A van den Essen","year":"1996","unstructured":"van den Essen, A., Hubbers, E.: Polynomial maps with strongly nilpotent Jacobian matrix and the Jacobian conjecture. Linear Algebra Appl. 247, 121\u2013132 (1996). https:\/\/doi.org\/10.1016\/0024-3795(95)00095-X","journal-title":"Linear Algebra Appl."},{"key":"5_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8440-2","volume-title":"Polynomial Automorphisms and the Jacobian Conjecture","author":"A van den Essen","year":"2000","unstructured":"van den Essen, A.: Polynomial Automorphisms and the Jacobian Conjecture. Springer, Basel (2000). https:\/\/doi.org\/10.1007\/978-3-0348-8440-2"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-030-25543-5_24","volume-title":"Computer Aided Verification","author":"F Frohn","year":"2019","unstructured":"Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 426\u2013444. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24"},{"key":"5_CR16","unstructured":"Frohn, F., Hark, M., Giesl, J.: On the decidability of termination for polynomial loops. CoRR abs\/1910.11588 (2019). https:\/\/arxiv.org\/abs\/1910.11588"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Barrett, C.W., Yang, J. (eds.) FMCAD 2019, pp. 221\u2013230 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019","DOI":"10.23919\/FMCAD.2019"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Biere, A., Parkerm D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 58\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"issue":"5","key":"5_CR19","doi-asserted-by":"publisher","first-page":"948","DOI":"10.1137\/S0097539793252687","volume":"24","author":"M Giesbrecht","year":"1995","unstructured":"Giesbrecht, M.: Nearly optimal algorithms for canonical matrix forms. SIAM J. Comput. 24(5), 948\u2013969 (1995). https:\/\/doi.org\/10.1137\/S0097539793252687","journal-title":"SIAM J. Comput."},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J. Autom. Reasoning"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-030-17502-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 147\u2013158 (2008). https:\/\/doi.org\/10.1145\/1328438.1328459","DOI":"10.1145\/1328438.1328459"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Hark, M., Frohn, F., Giesl, J.: Polynomial loops: beyond termination. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020. EPiC, vol. 73, pp. 279\u2013297 (2020). https:\/\/doi.org\/10.29007\/nxv1","DOI":"10.29007\/nxv1"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Hosseini, M., Ouaknine, J., Worrell, J.: Termination of linear loops over the integers. In: Baier, C., Chatzigiannakis, I., Flocchini, P., Leonardi, S. (eds.) ICALP 2019. LIPIcs, vol. 132, 118:1\u2013118:13 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.118","DOI":"10.4230\/LIPIcs.ICALP.2019.118"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Invariant generation for multi-path loops with polynomial assignments. In: Dillig, I., Palsberg, J. (eds.) VMCAI 2018. LNCS, vol. 10747, pp. 226\u2013246. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_11","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Kauers, M., Paule, P.: The Concrete Tetrahedron \u2013 Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-7091-0445-3","DOI":"10.1007\/978-3-7091-0445-3"},{"issue":"POPL","key":"5_CR27","doi-asserted-by":"publisher","first-page":"54:1","DOI":"10.1145\/3158142","volume":"2","author":"Z Kincaid","year":"2018","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 54:1\u201354:33 (2018). https:\/\/doi.org\/10.1145\/3158142","journal-title":"Proc. ACM Program. Lang."},{"issue":"POPL","key":"5_CR28","doi-asserted-by":"publisher","first-page":"55:1","DOI":"10.1145\/3290368","volume":"3","author":"Z Kincaid","year":"2019","unstructured":"Kincaid, Z., Breck, J., Cyphert, J., Reps, T.W.: Closed forms for numerical loops. Proc. ACM Program. Lang. 3(POPL), 55:1\u201355:29 (2019). https:\/\/doi.org\/10.1145\/3290368","journal-title":"Proc. ACM Program. Lang."},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about p-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249\u2013264. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Jobstmann, B., Ray, S. (eds.) FMCAD 2013, pp. 218\u2013225 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679413","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1007\/978-3-319-08867-9_52","volume-title":"Computer Aided Verification","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination Using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779\u2013796. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_52"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. Logical Method Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:16)2015","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-319-89963-3_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Leike","year":"2018","unstructured":"Leike, J., Heizmann, M.: Geometric nontermination arguments. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 266\u2013283. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_16"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Li, Y.: A recursive decision method for termination of linear programs. In: Zhi, L., Watt, S.M. (eds.) SNC 2014, pp. 97\u2013106 (2014). https:\/\/doi.org\/10.1145\/2631948.2631966","DOI":"10.1145\/2631948.2631966"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-319-46750-4_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"Y Li","year":"2016","unstructured":"Li, Y.: Termination of single-path polynomial loop programs. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 33\u201350. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_3"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-69483-2_8","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"Y Li","year":"2017","unstructured":"Li, Y.: Termination of semi-algebraic loop programs. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 131\u2013146. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_8"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.tcs.2017.03","volume":"681","author":"Y Li","year":"2017","unstructured":"Li, Y.: Witness to non-termination of linear programs. Theoret. Comput. Sci. 681, 75\u2013100 (2017). https:\/\/doi.org\/10.1016\/j.tcs.2017.03","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Neumann, E., Ouaknine, J., Worrell, J.: On ranking function synthesis and termination for polynomial programs. In: Konnov, I., Kov\u00e1cs, L. (eds.) CONCUR 2020. LIPIcs, vol. 171, pp. 15:1\u201315:15 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.15","DOI":"10.4230\/LIPIcs.CONCUR.2020.15"},{"key":"5_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2016","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-319-68167-2_22","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2017","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Synthesizing invariants by solving solvable loops. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 327\u2013343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_22"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Indyk, P. (ed.) SODA 2015, pp. 957\u2013969 (2015). https:\/\/doi.org\/10.1137\/19781611973730.65","DOI":"10.1137\/19781611973730.65"},{"issue":"1\u20132","key":"5_CR42","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s10107-016-1036-0","volume":"162","author":"AD Pia","year":"2017","unstructured":"Pia, A.D., Dey, S.S., Molinaro, M.: Mixed-integer quadratic programming is in NP. Math. Program. 162(1\u20132), 225\u2013240 (2017). https:\/\/doi.org\/10.1007\/s10107-016-1036-0","journal-title":"Math. Program."},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. J. Symbolic Comput. 13(3), 255\u2013300 (1992). https:\/\/doi.org\/10.1016\/S0747-7171(10)80003-3","DOI":"10.1016\/S0747-7171(10)80003-3"},{"issue":"2","key":"5_CR45","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. J. Symbolic Logic 14(2), 98\u2013114 (1949). https:\/\/doi.org\/10.2307\/2266510","journal-title":"J. Symbolic Logic"},{"issue":"02","key":"5_CR46","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1142\/S0129626496000200","volume":"06","author":"J-L Roch","year":"1996","unstructured":"Roch, J.-L., Villard, G.: Fast parallel computation of the Jordan normal form of matrices. Parallel Process. Lett. 06(02), 203\u2013212 (1996). https:\/\/doi.org\/10.1142\/S0129626496000200","journal-title":"Parallel Process. Lett."},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Roche, D.S.: What Can (and Can\u2019t) we Do with Sparse Polynomials?\u201d In: Kauers, M., Indyk, Ovchinnikov, A., Schost, \u00c9 (eds.) ISSAC 2018, pp. 25\u201330 (2018). https:\/\/doi.org\/10.1145\/3208976.3209027","DOI":"10.1145\/3208976.3209027"},{"key":"5_CR48","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundation. In: Gutierrez, J. (ed.) ISSAC 2004, pp. 266\u2013273 (2004). https:\/\/doi.org\/10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"issue":"4","key":"5_CR49","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symbolic Comput. 42(4), 443\u2013476 (2007). https:\/\/doi.org\/10.1016\/j.jsc.2007.01.002","journal-title":"J. Symbolic Comput."},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-11805-0_32","volume-title":"Graph Drawing","author":"M Schaefer","year":"2010","unstructured":"Schaefer, M.: Complexity of some geometric and topological problems. In: Eppstein, D., Gansner, E.R. (eds.) GD 2009. LNCS, vol. 5849, pp. 334\u2013344. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11805-0_32"},{"issue":"2","key":"5_CR51","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/s00224-015-9662-0","volume":"60","author":"M Schaefer","year":"2017","unstructured":"Schaefer, M., \u0160tefankovi\u010d, D.: Fixed points, Nash equilibria, and the existential theory of the reals. Theory Comput. Syst. 60(2), 172\u2013193 (2017). https:\/\/doi.org\/10.1007\/s00224-015-9662-0","journal-title":"Theory Comput. Syst."},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Originally appeared in 1951, University of California Press, Berkeley and Los Angeles, pp. 24\u201384. Springer, Vienna (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_3","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70\u201382. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6"},{"key":"5_CR54","unstructured":"TPDB (Termination Problems Data Base). http:\/\/termination-portal.org\/wiki\/TPDB"},{"issue":"11","key":"5_CR55","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1016\/j.jsc.2010.06.006","volume":"45","author":"B Xia","year":"2010","unstructured":"Xia, B., Zhang, Z.: Termination of linear programs with nonlinear constraints. J. Symbolic Comput. 45(11), 1234\u20131249 (2010). https:\/\/doi.org\/10.1016\/j.jsc.2010.06.006","journal-title":"J. Symbolic Comput."},{"key":"5_CR56","doi-asserted-by":"publisher","unstructured":"Xu, M., Li, Z.: Symbolic termination analysis of solvable loops. J. Symbolic Comput. 50, 28\u201349 (2013). https:\/\/doi.org\/10.1016\/jjsc.2012.05.005","DOI":"10.1016\/jjsc.2012.05.005"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-65474-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,13]],"date-time":"2021-01-13T13:43:31Z","timestamp":1610545411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-65474-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030654733","9783030654740"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-65474-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/sas-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic the event was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}