{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:00Z","timestamp":1787592240723,"version":"build-2736575974"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Rust has become a popular system programming language that strikes a balance between memory safety and performance. Rust\u2019s type system ensures the safety of low-level memory controls; however, a well-typed Rust program is not guaranteed to enjoy high performance. This article studies static analysis for resource consumption of Rust programs, aiming at understanding the performance of Rust programs. Although there have been tons of studies on static resource analysis, exploiting Rust\u2019s memory safety\u2014especially the borrow mechanisms and their properties\u2014to aid resource-bound analysis, remains unexplored.<\/jats:p>\n                  <jats:p>\n                    This article presents\n                    <jats:sc>RaRust<\/jats:sc>\n                    , a type-based linear resource-bound analysis for well-typed Rust programs.\n                    <jats:sc>RaRust<\/jats:sc>\n                    follows the methodology of automatic amortized resource analysis (AARA) to build a resource-aware type system. To support Rust\u2019s borrow mechanisms, including shared and mutable borrows,\n                    <jats:sc>RaRust<\/jats:sc>\n                    introduces shared and novel prophecy potentials to reason about borrows compositionally. To prove the soundness of\n                    <jats:sc>RaRust<\/jats:sc>\n                    , this article proposes Resource-Aware Borrow Calculus (RABC) as a variant of recently proposed Low-Level Borrow Calculus (LLBC). The experimental evaluation of a prototype implementation of\n                    <jats:sc>RaRust<\/jats:sc>\n                    demonstrates that\n                    <jats:sc>RaRust<\/jats:sc>\n                    is capable of inferring symbolic linear resource bounds for Rust programs featuring shared and mutable borrows, reborrows, heap-allocated data structures, loops, and recursion.\n                  <\/jats:p>","DOI":"10.1145\/3720492","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1406-1433","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8969-2805","authenticated-orcid":false,"given":"Qihao","family":"Lian","sequence":"first","affiliation":[{"name":"Peking University, Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education; School of Computer Science, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2418-7987","authenticated-orcid":false,"given":"Di","family":"Wang","sequence":"additional","affiliation":[{"name":"Peking University, Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education; School of Computer Science, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi and Leslie Lamport. 1988. The Existence of Refinement Mappings. In Logic in Computer Science (LICS\u201988). 165\u2013175. doi:10.1109\/LICS.1988.5115","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Elvira Albert Jes\u00fas Correas Fern\u00e1ndez and Guillermo Rom\u00e1n-D\u00edez. 2015. Non-Cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201915). 85\u2013100. doi:10.1007\/978-3-662-46681-0_6","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Diego Esteban Alonso-Blas and Samir Genaim. 2012. On the Limits of the Classical Approach to Cost Analysis. In Static Analysis Symp. (SAS\u201912). 405\u2013421. doi:10.1007\/978-3-642-33125-1_27","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2010. Amortised Resource Analysis with Separation Logic. In European Symp. on Programming (ESOP\u201910). 85\u2013103. doi:10.1007\/978-3-642-11957-6_6","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110287"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Ugo Dal Lago and Georg Moser. 2015. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Int. Conf. on Functional Programming (ICFP\u201915). 152\u2013164. doi:10.1145\/2784731.2784753","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Martin Avanzini and Georg Moser. 2013. A Combination Framework for Complexity. In Rewriting Techniques and Applications (RTA\u201913). 55\u201370. doi:10.4230\/LIPIcs.RTA.2013.55","DOI":"10.4230\/LIPIcs.RTA.2013.55"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"R\u00e9gis Blanc Thomas A. Henzinger Thibaud Hottelier and Laura Kov\u00e1cs. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Programming Artificial Intelligence and Reasoning (LPAR\u201910). 103\u2013118. doi:10.1007\/978-3-642-17511-4_7","DOI":"10.1007\/978-3-642-17511-4_7"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Jason Breck John Cyphert Zachary Kincaid and Thomas Reps. 2020. Templates and Recurrences: Better Together. In Prog. Lang. Design and Impl. (PLDI\u201920). 688\u2013702. doi:10.1145\/3385412.3386035","DOI":"10.1145\/3385412.3386035"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Marc Brockschmidt Fabian Emmes Stephan Falke Carsten Fuhs and J\u00fcrgen Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201914). doi:10.1007\/978-3-642-54862-8_10","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Quentin Carbonneaux Jan Hoffmann and Zhong Shao. 2015. Compositional Certified Resource Bounds. In Prog. Lang. Design and Impl. (PLDI\u201915). doi:10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Ezgi \u00c7i\u00e7ek Gilles Barthe Marco Gaboardi Deepak Garg and Jan Hoffmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL\u201917). 316\u2013329. doi:10.1145\/3009837.3009858","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Ezgi \u00c7i\u00e7ek Deepak Garg and Umut Acar. 2015. Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP\u201915).406\u2013431. doi:10.1007\/978-3-662-46669-8_17","DOI":"10.1007\/978-3-662-46669-8_17"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Karl Crary and Stephnie Weirich. 2000. Resource Bound Certification. In Princ. of Prog. Lang. (POPL\u201900). 184\u2013198. doi:10.1145\/325694.325716","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Princ. of Prog. Lang. (POPL\u201908). 133\u2013144. doi:10.1145\/1328438.1328457","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Norman Danner Daniel R. Licata and Ramyaa Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP\u201915). 140\u2013151. doi:10.1145\/2784731.2784749","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71322-7_8"},{"key":"e_1_3_2_21_1","volume-title":"Reasoning about Complexities in a Rust Verifier","author":"Engel Lowis","year":"2021","unstructured":"Lowis Engel. 2021. Reasoning about Complexities in a Rust Verifier. Master\u2019s thesis. ETH Z\u00fcrich."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Antonio Flores-Montoya and Reiner H\u00e4hnle. 2014. Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS\u201914). 275\u2013295. doi:10.1007\/978-3-319-12736-1_15","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"John Forrest Ted Ralphs Stefan Vigerske Haroldo Gambini Santos John Forrest Lou Hafer Bjarni Kristjansson jpfasano Edwin Straver Jan-Willem Miles Lubin rlougee a andre jpgoncal1 Samuel Brito h-i gassmann Cristina Matthew Saltzman tosttost Bruno Pitrus Fumiaki MATSUSHIMA Patrick Vossler Ron @ SWGY and to st. 2024. coin-or\/Cbc: Release releases\/2.10.12. doi:10.5281\/zenodo.13347261","DOI":"10.5281\/zenodo.13347261"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Florian Frohn Matthias Naaf Jera Hensel Marc Brockschmidt and J\u00fcrgen Giesl. 2016. Lower Runtime Bounds for Integer Programs. In Int. Joint Conf. on Automated Reasoning (IJCAR\u201916). doi:10.1007\/978-3-319-40229-1_37","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632852"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Krishna K. Mehra and Trishul Chilimbi. 2009. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In Princ. of Prog. Lang. (POPL\u201909). 127\u2013139. doi:10.1145\/1594834.1480898","DOI":"10.1145\/1594834.1480898"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL\u201917). 359\u2013373. doi:10.1145\/3009837.3009842","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604148"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000232"},{"key":"e_1_3_2_38_1","unstructured":"Infer. 2020. Cost: Runtime Complexity Analysis. Available on https:\/\/fbinfer.com\/docs\/checker-cost."},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473581"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Jason Breck Ashkan Forouhi Boroujeni and Thomas Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI\u201917). 248\u2013262. doi:10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290368"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Tristan Knoth Di Wang Nadia Polikarpova and Jan Hoffmann. 2019. Resource-Guided Program Synthesis. In Prog. Lang. Design and Impl. (PLDI\u201919). doi:10.1145\/3314221.3314602","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408988"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS\u201911). 133\u2013142. doi:10.1109\/LICS.2011.22","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Barbara Petit. 2013. The Geometry of Types. In Princ. of Prog. Lang. (POPL\u201913). 167\u2013178. doi:10.1145\/2429069.2429090","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Lorenz Leutgeb Georg Moser and Florian Zuleger. 2021. ATLAS: Automated Amortised Complexity Analysis of Selfadjusting Data Structures. In Computer Aided Verif. (CAV\u201921). 99\u2013122. doi:10.1007\/978-3-030-81688-9_5","DOI":"10.1007\/978-3-030-81688-9_5"},{"key":"e_1_3_2_54_1","unstructured":"Qihao Lian and Di Wang. 2025a. Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials. arXiv:2502.19810 [cs.PL] https:\/\/arxiv.org\/abs\/2502.19810"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","unstructured":"Qihao Lian and Di Wang. 2025b. Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials (Artifact). doi:10.5281\/zenodo.14801344","DOI":"10.5281\/zenodo.14801344"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lichtman and Jan Hoffmann. 2017. Arrays and References in Resource Aware ML. In Formal Struct. for Comput. and Deduction (FSCD\u201917). 26:1\u201326:20. doi:10.4230\/LIPIcs.FSCD.2017.26","DOI":"10.4230\/LIPIcs.FSCD.2017.26"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_59_1","unstructured":"Nicholas Nethercote. 2020. The Rust Performance Book. Available on https:\/\/nnethercote.github.io\/perf-book."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9277-6"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","unstructured":"Moritz Sinn Florian Zuleger and Helmut Veith. 2014. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verif. (CAV\u201914). 745\u2013761. doi:10.1007\/978-3-319-08867-9_50","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_2_66_1","volume-title":"Space Cost Analysis Using Sized Types","author":"Vasconcelos Pedro B.","year":"2008","unstructured":"Pedro B. Vasconcelos. 2008. Space Cost Analysis Using Sized Types. Ph.D. Dissertation. University of St Andrews."},{"key":"e_1_3_2_67_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker David","year":"2002","unstructured":"David Walker. 2002. Substructural Type Systems. In Advanced Topics in Types and Programming Languages. MIT Press."},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","unstructured":"Florian Zuleger Moritz Sinn Sumit Gulwani and Helmut Veith. 2011. Bound Analysis of Imperative Programs with the Size-Change Abstraction. In Static Analysis Symp. (SAS\u201911). 280\u2013297. doi:10.1007\/978-3-642-23702-7_22","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\/10.1145\/3720492","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720492","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:28:23Z","timestamp":1787588903000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720492"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":68,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720492"],"URL":"https:\/\/doi.org\/10.1145\/3720492","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}