{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:07:06Z","timestamp":1784200026326,"version":"3.55.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2106949"],"award-info":[{"award-number":["2106949"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    There are many state-of-the-art techniques for loop bound analysis. Most of them target an upper bound for a given program, and others find a lower bound.\n                    <jats:italic toggle=\"yes\">Exact<\/jats:italic>\n                    bound analysis still remains largely unexplored, but it offers new applications. To compute an\n                    <jats:italic toggle=\"yes\">exact<\/jats:italic>\n                    bound for a program it is necessary to reason about the possible values the program\u2019s inputs can take and how they relate to each other. Since inputs can vary on any given execution of the program, it makes the problem of computing an exact bound challenging. In this work, we present a new approach to find an exact bound by way of\n                    <jats:italic toggle=\"yes\">precondition synthesis<\/jats:italic>\n                    which iteratively considers under-approximations of a program under which the bound can be precomputed over initial values of program variables. For each precondition, our approach synthesizes a function over program variables such that when the function is applied to the initial values of the program variables, its output is an exact bound for the program. We reduce the precondition synthesis problem to that of\n                    <jats:italic toggle=\"yes\">safety verification<\/jats:italic>\n                    which lends its correctness guarantees to the exact bounds we compute. Our technique has been implemented in a tool called ELBA, and we show that it is effective on a set of challenging single loop benchmarks under Linear Integer Arithmetic.\n                  <\/jats:p>","DOI":"10.1145\/3729323","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1814-1837","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Exact Loop Bound Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6390-9778","authenticated-orcid":false,"given":"Daniel","family":"Riley","sequence":"first","affiliation":[{"name":"Florida State University, Tallahassee, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[{"name":"Florida State University, Tallahassee, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_40"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_2"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_3_2_9_2","first-page":"1027","article-title":"Semantic program alignment for equivalence checking","author":"Churchill Berkeley R.","year":"2019","unstructured":"Berkeley R. Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. 2019. Semantic program alignment for equivalence checking. In PLDI. ACM, 1027\u20131040.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_10_2","first-page":"58","article-title":"Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF","author":"Cimatti Alessandro","year":"2017","unstructured":"Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2017. Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European foint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10205), Axel Legay and Tiziana Margaria (Eds.). 58\u201375. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_4","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European foint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10205)"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000147"},{"key":"e_1_3_2_12_2","first-page":"415","article-title":"Termination proofs for systems code","author":"Cook Byron","year":"2006","unstructured":"Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI. ACM, 415\u2013426.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_14_2","first-page":"337","volume-title":"TACAS (LNCS, Vol. 4963)","author":"Mendon\u00e7a de Moura Leonardo","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS, Vol. 4963). Springer, 337\u2013340."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_32"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"e_1_3_2_18_2","first-page":"259","volume-title":"CAV, Part I (LNCS, Vol. 11561)","author":"Fedyukovich Grigory","year":"2019","unstructured":"Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. 2019. Quantified Invariants via SyntaxGuided Synthesis. In CAV, Part I (LNCS, Vol. 11561). Springer, 259\u2013277."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_3_2_24_2","first-page":"281","article-title":"Program analysis as constraint solving","author":"Gulwani Sumit","year":"2008","unstructured":"Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. 2008. Program analysis as constraint solving. In PLDI. ACM, 281\u2013292.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_18"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750392"},{"key":"e_1_3_2_28_2","first-page":"248","article-title":"Compositional recurrence analysis revisited","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas W. Reps. 2017. Compositional recurrence analysis revisited. In PLDI. ACM, 248\u2013262.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_29_2","first-page":"1","volume-title":"ICCAD","author":"Vediramana Krishnan Hari Govind","year":"2020","unstructured":"Hari Govind Vediramana Krishnan, Grigory Fedyukovich, and Arie Gurfinkel. 2020. Word Level Property Directed Reachability. In ICCAD. IEEE, 1\u20139."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456661"},{"key":"e_1_3_2_31_2","first-page":"788","article-title":"SLING: using dynamic analysis to infer program invariants in separation logic","author":"Le Ton Chanh","year":"2019","unstructured":"Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. 2019. SLING: using dynamic analysis to infer program invariants in separation logic. In PLDI. ACM, 788\u2013801.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-69483-2_9"},{"issue":"2","key":"e_1_3_2_33_2","first-page":"167","article-title":"Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption","volume":"18","author":"Darmawan Luthfi","year":"2018","unstructured":"Pedro L\u00f3pez-Garc\u00eda, Luthfi Darmawan, Maximiliano Klemen, Umer Liqat, Francisco Bueno, and Manuel V. Hermenegildo. 2018. Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption. TPLP 18, 2 (2018), 167\u2013223.","journal-title":"TPLP"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068416000442"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE49443.2020.00011"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"e_1_3_2_37_2","first-page":"605","article-title":"Counterexample-guided approach to finding numerical invariants","author":"Nguyen ThanhVu","year":"2017","unstructured":"ThanhVu Nguyen, Timos Antonopoulos, Andrew Ruef, and Michael Hicks. 2017. Counterexample-guided approach to finding numerical invariants. In ESEC\/FSE. ACM, 605\u2013615.","journal-title":"ESEC\/FSE"},{"key":"e_1_3_2_38_2","first-page":"246","article-title":"Termination proofs from tests","author":"Nori Aditya V.","year":"2013","unstructured":"Aditya V. Nori and Rahul Sharma. 2013. Termination proofs from tests. In ESEC\/FSE. ACM, 246\u2013256.","journal-title":"ESEC\/FSE. ACM"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_3_2_40_2","first-page":"42","article-title":"Data-Driven Precondition Inference with Learned Features","author":"Padhi Saswat","year":"2016","unstructured":"Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-Driven Precondition Inference with Learned Features. In PLDI. 42\u201356. https:\/\/doi.org\/10.1145\/2908080.2908099","journal-title":"PLDI"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549166"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"Daniel Riley and Grigory Fedyukovich. 2025. Artifact for Exact Loop Bound Analysis. https:\/\/doi.org\/10.5281\/zenodo.15199489","DOI":"10.1145\/3729323"},{"key":"e_1_3_2_43_2","first-page":"1203","volume-title":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021","author":"Fedyukovich Grigory","year":"2021","unstructured":"Sumanth Prabhu S, Grigory Fedyukovich, Kumar Madhukar, and Deepak D\u2019Souza. 2021. Specification synthesis with constrained Horn clauses. In PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 1203\u20131217. https:\/\/doi.org\/10.1145\/3453483.3454104"},{"key":"e_1_3_2_44_2","first-page":"295","article-title":"Dynamic inference of likely data preconditions over predicates by tree learning","author":"Sankaranarayanan Sriram","year":"2008","unstructured":"Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta. 2008. Dynamic inference of likely data preconditions over predicates by tree learning. In Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008. 295\u2013306.","journal-title":"Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_2_48_2","first-page":"1","article-title":"Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints","author":"Sinn Moritz","year":"2017","unstructured":"Moritz Sinn, Florian Zuleger, and Helmut Veith. 2017. Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints. Journal of Automated Reasoning (2017), 1\u201343. https:\/\/doi.org\/10.1007\/s10817-016-9402-4","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_49_2","first-page":"707","article-title":"A data-driven CHC solver","author":"Zhu He","year":"2018","unstructured":"He Zhu, Stephen Magill, and Suresh Jagannathan. 2018. A data-driven CHC solver. In PLDI. ACM, 707\u2013721.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729323","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729323","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:21Z","timestamp":1784196441000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729323"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":49,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729323"],"URL":"https:\/\/doi.org\/10.1145\/3729323","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}