{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:22:59Z","timestamp":1762816979261,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":26,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819542123"},{"type":"electronic","value":"9789819542130"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_13","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:17:53Z","timestamp":1762816673000},"page":"228-246","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synthesizing Loops from\u00a0Linear Ranking Functions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6932-8862","authenticated-orcid":false,"given":"Rui-Juan","family":"Jing","sequence":"first","affiliation":[]},{"given":"Yaru","family":"Yuan","sequence":"additional","affiliation":[]},{"given":"Yuxing","family":"Cai","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0693-0247","authenticated-orcid":false,"given":"Yi","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7412-7667","authenticated-orcid":false,"given":"Changbo","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"13_CR1","unstructured":"Bauer, A., et al.: Comprehensive exploration of synthetic data generation: a survey (2024)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1007\/11523468_109","volume-title":"Automata, Languages and Programming","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349\u20131361. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11523468_109"},{"key":"13_CR3","unstructured":"Chen, C., Chen, X., Keita, A., Moreno Maza, M., Xie, N.: Metafork: a compilation framework for concurrency models targeting hardware accelerators and its application to the generation of parametric CUDA kernels. In: Proceedings of 25th Annual International Conference on Computer Science and Software Engineering, CASCON 2015, Markham, Ontario, Canada, 2\u20134 November 2015, pp. 70\u201379. IBM\/ACM (2015)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.jsc.2015.11.008","volume":"75","author":"C Chen","year":"2016","unstructured":"Chen, C., Moreno Maza, M.: Quantifier elimination by cylindrical algebraic decomposition based on regular chains. J. Symb. Comput. 75, 74\u201393 (2016)","journal-title":"J. Symb. Comput."},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442\u2013454. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_36"},{"key":"13_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 de Moura","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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bull."},{"key":"13_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-69070-9_1","volume-title":"CASC 2024","author":"M England","year":"2024","unstructured":"England, M.: Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk). In: Boulier, F., Mou, C., Sadykov, T.M., Vorozhtsov, E.V. (eds.) CASC 2024. LNCS, vol. 14938, pp. 1\u201310. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-69070-9_1"},{"issue":"11","key":"13_CR10","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1145\/3422622","volume":"63","author":"I Goodfellow","year":"2020","unstructured":"Goodfellow, I., et al.: Generative adversarial networks. Commun. ACM 63(11), 139\u2013144 (2020)","journal-title":"Commun. ACM"},{"issue":"11","key":"13_CR11","doi-asserted-by":"publisher","first-page":"1206","DOI":"10.1016\/j.jsc.2005.09.012","volume":"41","author":"A Gr\u00f6\u00dflinger","year":"2006","unstructured":"Gr\u00f6\u00dflinger, A., Griebl, M., Lengauer, C.: Quantifier elimination in automatic loop parallelization. J. Symb. Comput. 41(11), 1206\u20131221 (2006)","journal-title":"J. Symb. Comput."},{"key":"13_CR12","first-page":"6840","volume":"33","author":"J Ho","year":"2020","unstructured":"Ho, J., Jain, A., Abbeel, P.: Denoising diffusion probabilistic models. Adv. Neural. Inf. Process. Syst. 33, 6840\u20136851 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"13_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-031-38499-8_18","volume-title":"CADE 2023","author":"P Hozzov\u00e1","year":"2023","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Norman, C., Voronkov, A.: Program synthesis in saturation. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 307\u2013324. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_18"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Amrollahi, D., Bj\u00f8rner, N., Kov\u00e1cs, L.: Algebra-based reasoning for loop synthesis. Form. Asp. Comput. 34(1) (2022)","DOI":"10.1145\/3527458"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Kenison, G., Kov\u00e1cs, L., Varonka, A.: From polynomial invariants to linear loops. In: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, ISSAC 2023, Troms\u00f8, Norway, 24\u201327 July 2023, pp. 398\u2013406. ACM (2023)","DOI":"10.1145\/3597066.3597109"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Kera, H., Ishihara, Y., Kambe, Y., Vaccon, T., Yokoyama, K.: Learning to compute gr\u00f6bner bases. In: Advances in Neural Information Processing Systems, vol.\u00a037, pp. 33141\u201333187. Curran Associates, Inc. (2024)","DOI":"10.52202\/079017-1044"},{"key":"13_CR17","unstructured":"Kuttler, K., Farah, I.: A first course in linear algebra. Lyryx Alberta (2017)"},{"key":"13_CR18","unstructured":"Lample, G., Charton, F.: Deep learning for symbolic mathematics. In: International Conference on Learning Representations (2020)"},{"key":"13_CR19","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"},{"issue":"1","key":"13_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2160910.2160912","volume":"34","author":"L Renganarayanan","year":"2012","unstructured":"Renganarayanan, L., Kim, D., Strout, M.M., Rajopadhye, S.: Parameterized loop tiling. ACM Trans. Program. Lang. Syst. (TOPLAS) 34(1), 1\u201341 (2012)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"13_CR21","volume-title":"The Foundations of Program Verification","author":"K Sieber","year":"2013","unstructured":"Sieber, K.: The Foundations of Program Verification. Springer, Cham (2013)"},{"issue":"9","key":"13_CR22","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/j.jsc.2006.06.004","volume":"41","author":"AW Strzebo\u0144ski","year":"2006","unstructured":"Strzebo\u0144ski, A.W.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021\u20131038 (2006)","journal-title":"J. Symb. Comput."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Sturm, T.: Thirty years of virtual substitution: foundations, techniques, applications. In: Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation, pp. 11\u201316 (2018)","DOI":"10.1145\/3208976.3209030"},{"issue":"7995","key":"13_CR24","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","volume":"625","author":"TH Trinh","year":"2024","unstructured":"Trinh, T.H., Wu, Y., Le, Q.V., He, H., Luong, T.: Solving olympiad geometry without human demonstrations. Nature 625(7995), 476\u2013482 (2024)","journal-title":"Nature"},{"issue":"1\u20132","key":"13_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1\u20132), 3\u201327 (1988)","journal-title":"J. Symb. Comput."},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2013the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8, 85\u2013101 (1997)","journal-title":"Appl. Algebra Eng. Commun. Comput."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:12Z","timestamp":1762816692000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}