{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:05:31Z","timestamp":1784768731728,"version":"3.55.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889"],"award-info":[{"award-number":["N00014-17-1-2889"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-14-2-0270,FA9750-15-C-0082"],"award-info":[{"award-number":["FA8750-14-2-0270,FA9750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100001395","name":"Wisconsin Alumni Research Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100001395","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. Our approach builds on classical techniques for analyzing the behavior of linear dynamical systems. It is well-known that a closed-form representation of the behavior of a linear dynamical system can always be expressed using algebraic numbers, but this approach can create formulas that present an obstacle for automated-reasoning tools. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing closed forms is decidable, yielding decision procedures for verifying safety and termination of a class of numerical loops over rational numbers. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).<\/jats:p>","DOI":"10.1145\/3290368","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Closed forms for numerical loops"],"prefix":"10.1145","volume":"3","author":[{"given":"Zachary","family":"Kincaid","sequence":"first","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Breck","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Cyphert","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA \/ GrammaTech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"1","article-title":"The Polytope-Collision Problem","volume":"24","author":"Almagor S.","year":"2017","unstructured":"S. Almagor , J. Ouaknine , and J. Worrell . 2017 . The Polytope-Collision Problem . In ICALP. 24 : 1 \u2013 24 :14. S. Almagor, J. Ouaknine, and J. Worrell. 2017. The Polytope-Collision Problem. In ICALP. 24:1\u201324:14.","journal-title":"ICALP."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00314-1"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_29"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_49"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"H. Comon and Y. Jurski. 1998. Multiple counters automata safety analysis and presburger arithmetic. In CAV. 268\u2013279.   H. Comon and Y. Jurski. 1998. Multiple counters automata safety analysis and presburger arithmetic. In CAV. 268\u2013279.","DOI":"10.1007\/BFb0028751"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS.   L. de Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"S. de Oliveira S. Bensalem and V. Prevosto. 2016. Polynomial Invariants by Linear Algebra. In ATVA. 479\u2013494.  S. de Oliveira S. Bensalem and V. Prevosto. 2016. Polynomial Invariants by Linear Algebra. In ATVA. 479\u2013494.","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD.   A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD.","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"A. Finkel and J. Leroux. 2002. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In FST TCS. 145\u2013156.   A. Finkel and J. Leroux. 2002. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In FST TCS. 145\u2013156.","DOI":"10.1007\/3-540-36206-1_14"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"A. Gurfinkel T. Kahsai A. Komuravelli and J.A. Navas. 2015. The SeaHorn Verification Framework. In CAV.  A. Gurfinkel T. Kahsai A. Komuravelli and J.A. Navas. 2015. The SeaHorn Verification Framework. In CAV.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_15_1","unstructured":"V. Halava T. Harju M. Hirvensalo and J. Karhum\u00e4d\u00e4ki. 2005. Skolem\u2019s Problem \u2013 On the Border between Decidability and Undecidability. Technical Report. Turku Center for Computer Science.  V. Halava T. Harju M. Hirvensalo and J. Karhum\u00e4d\u00e4ki. 2005. Skolem\u2019s Problem \u2013 On the Border between Decidability and Undecidability. Technical Report. Turku Center for Computer Science."},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"M. Heizmann Y.-F. Chen D. Dietsch M. Greitschus J. Hoenicke Y. Li A. Nutz B. Musa C. Schilling T. Schindler and A. Podelski. 2018. Ultimate Automizer and the Search for Perfect Interpolants. In TACAS. 447\u2013451.  M. Heizmann Y.-F. Chen D. Dietsch M. Greitschus J. Hoenicke Y. Li A. Nutz B. Musa C. Schilling T. Schindler and A. Podelski. 2018. Ultimate Automizer and the Search for Perfect Interpolants. In TACAS. 447\u2013451.","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087604.3087623"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"A. Humenberger M. Jaroschek and L. Kov\u00e1cs. 2018. Invariant Generation for Multi-Path Loops with Polynomial Assignments. In VMCAI. 226\u2013246.  A. Humenberger M. Jaroschek and L. Kov\u00e1cs. 2018. Invariant Generation for Multi-Path Loops with Polynomial Assignments. In VMCAI. 226\u2013246.","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535843"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6496"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/3929.3939"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid. 2018. Numerical Invariants via Abstract Machines. In SAS.  Z. Kincaid. 2018. Numerical Invariants via Abstract Machines. In SAS.","DOI":"10.1007\/978-3-319-99725-4_3"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_42"},{"key":"e_1_2_2_27_1","unstructured":"L. Kov\u00e1cs. 2008. Reasoning Algebraically About P-Solvable Loops. In TACAS.  L. Kov\u00e1cs. 2008. Reasoning Algebraically About P-Solvable Loops. In TACAS."},{"key":"e_1_2_2_28_1","first-page":"52","article-title":"Finding polynomial invariants for imperative loops in the theorema system","volume":"6","author":"Kov\u00e1cs L.","year":"2006","unstructured":"L. Kov\u00e1cs and T. Jebelean . 2006 . Finding polynomial invariants for imperative loops in the theorema system . Proc. of Verify 6 (2006), 52 \u2013 67 . L. Kov\u00e1cs and T. Jebelean. 2006. Finding polynomial invariants for imperative loops in the theorema system. Proc. of Verify 6 (2006), 52\u201367.","journal-title":"Proc. of Verify"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"L. Kov\u00e1cs N. Popov and T. Jebelean. 2006. Combining Logic and Algebraic Techniques for Program Verification in Theorema. In ISoLA. IEEE 67\u201374.  L. Kov\u00e1cs N. Popov and T. Jebelean. 2006. Combining Logic and Algebraic Techniques for Program Verification in Theorema. In ISoLA. IEEE 67\u201374.","DOI":"10.1109\/ISoLA.2006.46"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457454"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"R. Loos and V. Weispfenning. 1993. Applying linear quantifier elimination. The computer journal 36 5 (1993) 450\u2013462.  R. Loos and V. Weispfenning. 1993. Applying linear quantifier elimination. The computer journal 36 5 (1993) 450\u2013462.","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"e_1_2_2_32_1","volume-title":"European Symp. on Programming. 560\u2013588","author":"Min\u00e9 A.","unstructured":"A. Min\u00e9 , J. Breck , and T. W. Reps . 2016. An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs . In European Symp. on Programming. 560\u2013588 . A. Min\u00e9, J. Breck, and T. W. Reps. 2016. An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs. In European Symp. on Programming. 560\u2013588."},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"J. Ouaknine J. Sousa Pinto and J. Worrell. 2015. On Termination of Integer Linear Loops. In SODA. 957\u2013969.   J. Ouaknine J. Sousa Pinto and J. Worrell. 2015. On Termination of Integer Linear Loops. In SODA. 957\u2013969.","DOI":"10.1137\/1.9781611973730.65"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"J. Ouaknine and J. Worrell. 2012. Decision Problems for Linear Recurrence Sequences. In RP.   J. Ouaknine and J. Worrell. 2012. Decision Problems for Linear Recurrence Sequences. In RP.","DOI":"10.1007\/978-3-642-33512-9_3"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"E. Rodr\u00edguez-Carbonell and D. Kapur. 2004. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In ISSAC. 266\u2013273.  E. Rodr\u00edguez-Carbonell and D. Kapur. 2004. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In ISSAC. 266\u2013273.","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_2_2_38_1","volume-title":"NTL: A library for doing number theory.","author":"Shoup V.","year":"2018","unstructured":"V. Shoup . 2018 . NTL: A library for doing number theory. (2018). http:\/\/www.shoup.net\/ntl\/ V. Shoup. 2018. NTL: A library for doing number theory. (2018). http:\/\/www.shoup.net\/ntl\/"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1525\/9780520348097"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"A. Tiwari. 2004. Termination of Linear Programs. In CAV.  A. Tiwari. 2004. Termination of Linear Programs. In CAV.","DOI":"10.1007\/978-3-540-27813-9_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290368","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290368","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290368","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290368"],"URL":"https:\/\/doi.org\/10.1145\/3290368","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}