{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T13:05:32Z","timestamp":1768741532755,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Loops are inductive constructs, which make them difficult to analyze and verify in general. One approach is to represent the inductive behaviors of the program variables in a loop by recurrences and try to solve them for closed-form solutions. These solutions can then be used to generate invariants or directly fed into an SMT-based verifier. One problem with this approach is that if a loop contains nondeterministic choices or complex operations such as non-linear assignments, then recurrences for program variables may not exist or may have no closed-form solutions. In such cases, an alternative is to generate recurrences for expressions, and there has been recent work along this line. In this paper, we further work in this direction and propose a template-based method for extracting polynomial expressions that satisfy some c-finite recurrences. While in general there are possibly infinitely many such polynomials for a given loop, we show that the desired polynomials form a finite union of vector spaces. We propose an algorithm for computing the bases of the vector spaces, and identify two cases where the bases can be computed efficiently. To demonstrate the usefulness of our results, we implemented a prototype system based on one of the special cases, and integrated it into an SMT-based verifier. Our experimental results show that the new verifier can now verify programs with non-linear properties.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_20","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"409-430","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Polynomial Expressions with\u00a0C-Finite Recurrences in\u00a0Loops with\u00a0Nested Nondeterministic Branches"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1930-4771","authenticated-orcid":false,"given":"Chenglin","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3141-8675","authenticated-orcid":false,"given":"Fangzhen","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Amrollahi, D., Bartocci, E., Kenison, G., Kov\u00e1cs, L., Moosbrugger, M., Stankovi\u010d, M.: Solving invariant generation for\u00a0unsolvable loops. In: Singh, G., Urban, C. (eds.) SAS 2022. LNCS, pp. 19\u201343. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: sv-comp 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"20_CR3","doi-asserted-by":"publisher","unstructured":"Cyphert, J., Breck, J., Kincaid, Z., Reps, T.W.: Refinement of path expressions for static analysis. Proc. ACM Program. Lang. 3(POPL), 45:1\u201345:29 (2019). https:\/\/doi.org\/10.1145\/3290358","DOI":"10.1145\/3290358"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Cyphert, J., Kincaid, Z.: Solvable polynomial ideals: the ideal reflection for program analysis. arXiv preprint arXiv:2311.04092 (2023)","DOI":"10.1145\/3632867"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Darke, P., Agrawal, S., Venkatesh, R.: VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg, pp. 458\u2013462. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_32","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"20_CR7","doi-asserted-by":"crossref","DOI":"10.1090\/surv\/104","volume-title":"Recurrence sequences","author":"G Everest","year":"2003","unstructured":"Everest, G., van der Poorten, A.J., Shparlinski, I., Ward, T., et al.: Recurrence sequences, vol. 104. American Mathematical Society Providence, RI (2003)"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Heizmann, M., et al.: Ultimate automizer with SMTInterpol: (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, 16\u201324 March 2013, pp. 641\u2013643. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_53","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 69\u201385. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Horn, R.A., Johnson, C.R.: Matrix Analysis. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139020411"},{"key":"20_CR11","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.: Compositional recurrence analysis revisited. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), pp. 248-262. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.: Compositional recurrence analysis revisited. SIGPLAN Not. 52(6), 248\u2013262 (2017). https:\/\/doi.org\/10.1145\/3140587.3062373","DOI":"10.1145\/3140587.3062373"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Cyphert, J., Reps, T.: Closed forms for numerical loops. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290368","DOI":"10.1145\/3290368"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 1\u201333 (2017)","DOI":"10.1145\/3158142"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Koh, N., Zhu, S.: When less is more: Consequence-finding in a weak theory of arithmetic. Proc. ACM Program. Lang. 7(POPL), 1275\u20131307 (2023)","DOI":"10.1145\/3571237"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 249\u2013264. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Lin, F.: A formalization of programs in first-order logic with a discrete linear order. Artif. Intell. 235, 1\u201325 (2016). https:\/\/doi.org\/10.1016\/j.artint.2016.01.014","DOI":"10.1016\/j.artint.2016.01.014"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Lin, F.: Machine theorem discovery. AI Magazine 39(2), 53\u201359 (2018). https:\/\/www.aaai.org\/ojs\/index.php\/aimagazine\/article\/view\/2794","DOI":"10.1609\/aimag.v39i2.2794"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"Rajkhowa, P., Lin, F.: VIAP 1.1: (Competition Contribution). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, 6\u201311 April 2019, Proceedings, Part III, pp. 250\u2013255. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_23","DOI":"10.1007\/978-3-030-17502-3_23"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification: 31st International Conference, CAV 2019, New York City, 15\u201318 July 2019, Proceedings, Part II, pp. 97\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"issue":"OOPSLA1","key":"20_CR21","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3586028","volume":"7","author":"C Wang","year":"2023","unstructured":"Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: the periodic case. Proc. ACM Program. Lang. 7(OOPSLA1), 28\u201355 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"20_CR22","unstructured":"Wendler, P., Beyer, D.: Bench exec 3.16 (2023). https:\/\/github.com\/sosy-lab\/benchexec"},{"key":"20_CR23","unstructured":"Wolfram, S., et\u00a0al.: The MATHEMATICA\u00ae Book, Version 4. Cambridge University Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:04:34Z","timestamp":1721934274000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}