{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T18:33:42Z","timestamp":1781375622708,"version":"3.54.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-14-2-0270,FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-14-2-0270,FA8750-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":"publisher","award":["Grant"],"award-info":[{"award-number":["Grant"]}],"id":[{"id":"10.13039\/100001395","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Rajiv and Ritu Batra","award":["Gift"],"award-info":[{"award-number":["Gift"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Automatic generation of non-linear loop invariants is a long-standing challenge in program analysis, with many applications. For instance, reasoning about exponentials provides a way to find invariants of digital-filter programs, and reasoning about polynomials and\/or logarithms is needed for establishing invariants that describe the time or memory usage of many well-known algorithms. An appealing approach to this challenge is to exploit the powerful recurrence-solving techniques that have been developed in the field of computer algebra, which can compute exact characterizations of non-linear repetitive behavior. However, there is a gap between the capabilities of recurrence solvers and the needs of program analysis: (1) loop bodies are not merely systems of recurrence relations---they may contain conditional branches, nested loops, non-deterministic assignments, etc., and (2) a client program analyzer must be able to reason about the closed-form solutions produced by a recurrence solver (e.g., to prove assertions).<\/jats:p>\n          <jats:p>This paper presents a method for generating non-linear invariants of general loops based on analyzing recurrence relations. The key components are an abstract domain for reasoning about non-linear arithmetic, a semantics-based method for extracting recurrence relations from loop bodies, and a recurrence solver that avoids closed forms that involve complex or irrational numbers. Our technique has been implemented in a program analyzer that can analyze general loops and mutually recursive procedures. Our experiments show that our technique shows promise for non-linear assertion-checking and resource-bound generation.<\/jats:p>","DOI":"10.1145\/3158142","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Non-linear reasoning for invariant synthesis"],"prefix":"10.1145","volume":"2","author":[{"given":"Zachary","family":"Kincaid","sequence":"first","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Cyphert","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Breck","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA \/ GrammaTech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93583"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.002"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_2_2_6_1","volume-title":"P URRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis. CoRR abs\/cs\/0512056","author":"Bagnara R.","year":"2005","unstructured":"R. Bagnara , A. Pescetti , A. Zaccagnini , and E. Zaffanella . 2005 a. P URRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis. CoRR abs\/cs\/0512056 (2005). R. Bagnara, A. Pescetti, A. Zaccagnini, and E. Zaffanella. 2005a. P URRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis. CoRR abs\/cs\/0512056 (2005)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_4"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"e_1_2_2_10_1","volume-title":"Introduction to the Operational Calculus","author":"Berg L.","unstructured":"L. Berg . 1967. Introduction to the Operational Calculus . North-Holland Publishing Co. , Amsterdam . L. Berg. 1967. Introduction to the Operational Calculus. North-Holland Publishing Co., Amsterdam."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_2_12_1","volume-title":"ABC: Algebraic Bound Computation for Loops. In Int. Conf. on Logic for Programming, Art. Intell., and Reasoning. 103\u2013118","author":"Blanc R.","unstructured":"R. Blanc , T. A. Henzinger , T. Hottelier , and L. Kov\u00e1cs . 2010 . ABC: Algebraic Bound Computation for Loops. In Int. Conf. on Logic for Programming, Art. Intell., and Reasoning. 103\u2013118 . R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kov\u00e1cs. 2010. ABC: Algebraic Bound Computation for Loops. In Int. Conf. on Logic for Programming, Art. Intell., and Reasoning. 103\u2013118."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_43"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088216.1088219"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"J. S. Cohen. 2003. Computer Algebra and Symbolic Computation: Mathematical Methods. A K Peters\/CRC Press.  J. S. Cohen. 2003. Computer Algebra and Symbolic Computation: Mathematical Methods. A K Peters\/CRC Press.","DOI":"10.1201\/9781439863701"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_22"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. 1978. Automatic Discovery of Linear Constraints Among Variables of a Program. In POPL.  P. Cousot and N. Halbwachs. 1978. Automatic Discovery of Linear Constraints Among Variables of a Program. In POPL.","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16721-3"},{"key":"e_1_2_2_23_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_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1857914.1857917"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_2_28_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_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_4"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56287-7_95"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_35"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_26"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"M. Heizmann J. Christ D. Dietsch E. Ermis J. Hoenicke M. Lindenmann A. Nutz C. Schilling and A. Podelski. 2013. Ultimate Automizer with SMTInterpol (Competition Contribution). In TACAS.  M. Heizmann J. Christ D. Dietsch E. Ermis J. Hoenicke M. Lindenmann A. Nutz C. Schilling and A. Podelski. 2013. Ultimate Automizer with SMTInterpol (Competition Contribution). In TACAS.","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087604.3087623"},{"key":"e_1_2_2_38_1","first-page":"3","article-title":"Hypernumbers","volume":"77","author":"M.","year":"1983","unstructured":"J.-G.- M. 1983 . Hypernumbers . I. Algebra. Studia Math. 77 (1983), 3 \u2013 16 . matwbn.icm.edu.pl\/ksiazki\/sm\/sm77\/sm7712.pdf Originally published in Polish in 1944. J.-G.-M. 1983. Hypernumbers. I. Algebra. Studia Math. 77 (1983), 3\u201316. matwbn.icm.edu.pl\/ksiazki\/sm\/sm77\/sm7712.pdf Originally published in Polish in 1944.","journal-title":"I. Algebra. Studia Math."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535843"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"M. Kauers and P. Paule. 2011. The Concrete Tetrahedron. SpringerWienNewYork.  M. Kauers and P. Paule. 2011. The Concrete Tetrahedron. SpringerWienNewYork.","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_43_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_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_2_2_49_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_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009864"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_2_2_55_1","unstructured":"H. Wilf. 1994. Generatingfunctionology 2nd. Ed. Academic Press. www.math.upenn.edu\/ wilf\/gfologyLinked2.pdf.  H. Wilf. 1994. Generatingfunctionology 2nd. Ed. Academic Press. www.math.upenn.edu\/ wilf\/gfologyLinked2.pdf."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158142","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158142","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158142"],"URL":"https:\/\/doi.org\/10.1145\/3158142","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}