{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T18:33:41Z","timestamp":1781375621644,"version":"3.54.1"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>In program verification, one method for reasoning about loops is to convert them into sets of recurrences, and  \n then try to solve these recurrences by computing their closed-form solutions.  \n While there are solvers for computing closed-form solutions to these recurrences,  \n their capabilities are limited when the recurrences have  \n conditional expressions, which arise when the body of a loop contains  \n conditional statements.  \n In this paper, we take a step towards solving these recurrences. Specifically, we consider what we call  \n conditional linear recurrences and show that given such a recurrence and an initial value, if the  \n index sequence generated by the recurrence on the initial value is what we call ultimately periodic,  \n then it has a closed-form solution. However, checking whether such a sequence is  \n ultimately periodic is undecidable so we propose a heuristic \"generate and verify\" algorithm for  \n checking the ultimate periodicity of the sequence and computing closed-form solutions at the same time.  \n We implemented a solver based on this algorithm, and  \n our experiments show that a straightforward program verifier based on our solver and using the SMT solver Z3  \n is effective in verifying properties of many benchmark programs that contain conditional statements in their loops,  \n and compares favorably to other recurrence-based verification tools. Finally, we also consider extending  \n our results to computing closed-form solutions of recurrences with unknown initial values.<\/jats:p>","DOI":"10.1145\/3586028","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"28-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Solving Conditional Linear Recurrences for Program Verification: The Periodic Case"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1930-4771","authenticated-orcid":false,"given":"Chenglin","family":"Wang","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3141-8675","authenticated-orcid":false,"given":"Fangzhen","family":"Lin","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"COMP 2021 - 10th International Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2021\/index.php","unstructured":"2021. COMP 2021 - 10th International Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2021\/index.php 2021. COMP 2021 - 10th International Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2021\/index.php"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386035"},{"key":"e_1_2_1_5_1","volume-title":"Theorem proving in arithmetic without multiplication. Machine intelligence, 7, 91-99","author":"Cooper David C","year":"1972","unstructured":"David C Cooper . 1972. Theorem proving in arithmetic without multiplication. Machine intelligence, 7, 91-99 ( 1972 ), 300. David C Cooper. 1972. Theorem proving in arithmetic without multiplication. Machine intelligence, 7, 91-99 (1972), 300."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290358"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11439-2_9"},{"key":"e_1_2_1_13_1","volume-title":"Matrix analysis","author":"Horn Roger A","unstructured":"Roger A Horn and Charles R Johnson . 2012. Matrix analysis . Cambridge university press . Roger A Horn and Charles R Johnson. 2012. Matrix analysis. Cambridge university press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535843"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290368"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.014"},{"key":"e_1_2_1_21_1","article-title":"Mathematical theory of computation","volume":"44","author":"Manna Zohar","year":"1979","unstructured":"Zohar Manna . 1979 . Mathematical theory of computation . Journal of Symbolic Logic , 44 , 1 (1979). Zohar Manna. 1979. Mathematical theory of computation. Journal of Symbolic Logic, 44, 1 (1979).","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_3"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Marko Petkovsek Herbert S. Wilf and Doron Zeilberger. 1996. A = B. Wellesley Mass. : A K Peters. \t\t\t\t  Marko Petkovsek Herbert S. Wilf and Doron Zeilberger. 1996. A = B. Wellesley Mass. : A K Peters.","DOI":"10.1201\/9781439864500"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.14711\/thesis-991012758169203412"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_23"},{"key":"e_1_2_1_27_1","volume-title":"The maple handbook: maple V release 4","author":"Redfern Darren","unstructured":"Darren Redfern . 2012. The maple handbook: maple V release 4 . Springer Science & Business Media . Darren Redfern. 2012. The maple handbook: maple V release 4. Springer Science & Business Media."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554354"},{"key":"e_1_2_1_30_1","volume-title":"The MATHEMATICA\u00ae book, version 4","author":"Wolfram Stephen","unstructured":"Stephen Wolfram . 1999. The MATHEMATICA\u00ae book, version 4 . Cambridge university press . Stephen Wolfram. 1999. The MATHEMATICA\u00ae book, version 4. Cambridge university press."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586028","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586028","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586028"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":30,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586028"],"URL":"https:\/\/doi.org\/10.1145\/3586028","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}