{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:55:13Z","timestamp":1769748913738,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2007024, CCF-2312262, and CCF-2312263"],"award-info":[{"award-number":["CCF-2007024, CCF-2312262, and CCF-2312263"]}],"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":[[2023,10,16]]},"abstract":"<jats:p>A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption.<\/jats:p>\n          <jats:p>This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain is challenging because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to that specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm.<\/jats:p>\n          <jats:p>We have implemented our inference algorithm in two different systems, targeting programs written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations.<\/jats:p>","DOI":"10.1145\/3622858","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1705-1728","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Inference of Resource Management Specifications"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4417-9416","authenticated-orcid":false,"given":"Narges","family":"Shadab","sequence":"first","affiliation":[{"name":"University of California, Riverside, Riverside, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5961-8142","authenticated-orcid":false,"given":"Pritam","family":"Gharat","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bengaluru, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6697-0219","authenticated-orcid":false,"given":"Shrey","family":"Tiwari","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bengaluru, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9379-277X","authenticated-orcid":false,"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3185-2340","authenticated-orcid":false,"given":"Martin","family":"Kellogg","sequence":"additional","affiliation":[{"name":"New Jersey Institute of Technology, Newark, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4446-4777","authenticated-orcid":false,"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4359-9378","authenticated-orcid":false,"given":"Akash","family":"Lal","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bengaluru, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7993-302X","authenticated-orcid":false,"given":"Manu","family":"Sridharan","sequence":"additional","affiliation":[{"name":"University of California, Riverside, Riverside, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.188.2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158103"},{"key":"e_1_2_1_3_1","volume-title":"Resource Leak Checker for must-call obligations. https:\/\/checkerframework.org\/manual\/#resource-leak-checker Accessed","year":"2023","unstructured":"2023. Resource Leak Checker for must-call obligations. https:\/\/checkerframework.org\/manual\/#resource-leak-checker Accessed 29 July 2023 2023. Resource Leak Checker for must-call obligations. https:\/\/checkerframework.org\/manual\/#resource-leak-checker Accessed 29 July 2023"},{"key":"e_1_2_1_4_1","volume-title":"Checker Framework Whole-Program Inference. https:\/\/checkerframework.org\/manual\/#whole-program-inference Accessed","year":"2023","unstructured":"2023. Checker Framework Whole-Program Inference. https:\/\/checkerframework.org\/manual\/#whole-program-inference Accessed 28 March 2023 2023. Checker Framework Whole-Program Inference. https:\/\/checkerframework.org\/manual\/#whole-program-inference Accessed 28 March 2023"},{"key":"e_1_2_1_5_1","volume-title":"OOPSLA \u201998: Object-Oriented Programming Systems, Languages, and Applications.","author":"Clarke David G.","unstructured":"David G. Clarke , John M. Potter , and James Noble . 1998. Ownership types for flexible alias protection . In OOPSLA \u201998: Object-Oriented Programming Systems, Languages, and Applications. Vancouver, BC , Canada . 48\u201364. David G. Clarke, John M. Potter, and James Noble. 1998. Ownership types for flexible alias protection. In OOPSLA \u201998: Object-Oriented Programming Systems, Languages, and Applications. Vancouver, BC, Canada. 48\u201364."},{"key":"e_1_2_1_6_1","volume-title":"Analyzing data flow in C#. https:\/\/codeql.github.com\/docs\/codeql-language-guides\/analyzing-data-flow-in-csharp\/ Accessed","year":"2023","unstructured":"2023. Analyzing data flow in C#. https:\/\/codeql.github.com\/docs\/codeql-language-guides\/analyzing-data-flow-in-csharp\/ Accessed 28 March 2023 2023. Analyzing data flow in C#. https:\/\/codeql.github.com\/docs\/codeql-language-guides\/analyzing-data-flow-in-csharp\/ Accessed 28 March 2023"},{"key":"e_1_2_1_7_1","volume-title":"Avoiding resource leaks. hhttps:\/\/help.eclipse.org\/2023-03\/index.jsp?topic=org.eclipse.jdt.doc.usertaskstask-avoiding_resource_leaks.htm Accessed","author":"Eclipse","year":"2023","unstructured":"Eclipse developers. 2023. Avoiding resource leaks. hhttps:\/\/help.eclipse.org\/2023-03\/index.jsp?topic=org.eclipse.jdt.doc.usertaskstask-avoiding_resource_leaks.htm Accessed 24 March 2023 Eclipse developers. 2023. Avoiding resource leaks. hhttps:\/\/help.eclipse.org\/2023-03\/index.jsp?topic=org.eclipse.jdt.doc.usertaskstask-avoiding_resource_leaks.htm Accessed 24 March 2023"},{"key":"e_1_2_1_8_1","unstructured":"accessed 2023. Entity Framework Core. https:\/\/github.com\/dotnet\/efcore#entity-framework-core \t\t\t\t  accessed 2023. Entity Framework Core. https:\/\/github.com\/dotnet\/efcore#entity-framework-core"},{"key":"e_1_2_1_9_1","volume-title":"International Symposium on Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity","author":"Flanagan Cormac","year":"2001","unstructured":"Cormac Flanagan and K. Rustan M. Leino . 2001 . Houdini, an annotation assistant for ESC\/Java. In FME \u201901 : International Symposium on Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity . Berlin, Germany. 500\u2013517. Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an annotation assistant for ESC\/Java. In FME \u201901: International Symposium on Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity. Berlin, Germany. 500\u2013517."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_2_1_11_1","unstructured":"Pritam Gharat Narges Shadab Shrey Tiwari Shuvendu Lahiri and Akash Lal. 2023. Resource Leak Checker (RLC#) for C# code using CodeQL. https:\/\/github.com\/microsoft\/global-resource-leaks-codeql \t\t\t\t  Pritam Gharat Narges Shadab Shrey Tiwari Shuvendu Lahiri and Akash Lal. 2023. Resource Leak Checker (RLC#) for C# code using CodeQL. https:\/\/github.com\/microsoft\/global-resource-leaks-codeql"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134319"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236051"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_15_1","volume-title":"https:\/\/github.com\/microsoft\/infersharp\/wiki\/InferSharp:-A-Scalable-Code-Analytics-Tool-for-.NET Accessed","author":"InferSharp InferSharp","year":"2023","unstructured":"InferSharp developers. 2023. InferSharp . https:\/\/github.com\/microsoft\/infersharp\/wiki\/InferSharp:-A-Scalable-Code-Analytics-Tool-for-.NET Accessed 24 March 2023 InferSharp developers. 2023. InferSharp. https:\/\/github.com\/microsoft\/infersharp\/wiki\/InferSharp:-A-Scalable-Code-Analytics-Tool-for-.NET Accessed 24 March 2023"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290339"},{"key":"e_1_2_1_17_1","volume-title":"ASE 2023: Proceedings of the 38th Annual International Conference on Automated Software Engineering","author":"Kellogg Martin","unstructured":"Martin Kellogg , Daniel Daskiewicz , Loi Ngo Duc Nguyen , Muyeed Ahmed , and Michael D. Ernst . 2023. Pluggable type inference for free . In ASE 2023: Proceedings of the 38th Annual International Conference on Automated Software Engineering . Luxembourg. Martin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed, and Michael D. Ernst. 2023. Pluggable type inference for free. In ASE 2023: Proceedings of the 38th Annual International Conference on Automated Software Engineering. Luxembourg."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468576"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.8.2.22"},{"key":"e_1_2_1_20_1","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press. https:\/\/doc.rust-lang.org\/stable\/book\/ \t\t\t\t  Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press. https:\/\/doc.rust-lang.org\/stable\/book\/"},{"key":"e_1_2_1_21_1","unstructured":"accessed 2023. Lucene.NET is a high performance search library for .NET. https:\/\/lucenenet.apache.org\/ \t\t\t\t  accessed 2023. Lucene.NET is a high performance search library for .NET. https:\/\/lucenenet.apache.org\/"},{"key":"e_1_2_1_22_1","volume-title":"accessed","year":"2023","unstructured":"Microsoft. accessed 2023 . CodeQL. https:\/\/codeql.github.com Microsoft. accessed 2023. CodeQL. https:\/\/codeql.github.com"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373104"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510038"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485488"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1104.003.0005"},{"key":"e_1_2_1_28_1","volume-title":"https:\/\/pmd.sourceforge.io\/pmd-6.55.0\/pmd_rules_java_errorprone.html#closeresource Accessed","author":"CloseResource PMD","year":"2023","unstructured":"PMD developers. 2023. CloseResource . https:\/\/pmd.sourceforge.io\/pmd-6.55.0\/pmd_rules_java_errorprone.html#closeresource Accessed 24 March 2023 PMD developers. 2023. CloseResource. https:\/\/pmd.sourceforge.io\/pmd-6.55.0\/pmd_rules_java_errorprone.html#closeresource Accessed 24 March 2023"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409715"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8333055"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_32_1","volume-title":"The Design and Evolution of C++","author":"Stroustrup Bjarne","unstructured":"Bjarne Stroustrup . 1994. The Design and Evolution of C++ . Addison-Wesley , Reading, Massachusetts . Bjarne Stroustrup. 1994. The Design and Evolution of C++. Addison-Wesley, Reading, Massachusetts."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806876"},{"key":"e_1_2_1_34_1","volume-title":"International Conference on Formal Methods for Open Object-Based Distributed Systems. 319\u2013333","author":"Vogels Fr\u00e9d\u00e9ric","year":"2011","unstructured":"Fr\u00e9d\u00e9ric Vogels , Bart Jacobs , Frank Piessens , and Jan Smans . 2011 . Annotation inference for separation logic based verifiers . In International Conference on Formal Methods for Open Object-Based Distributed Systems. 319\u2013333 . Fr\u00e9d\u00e9ric Vogels, Bart Jacobs, Frank Piessens, and Jan Smans. 2011. Annotation inference for separation logic based verifiers. In International Conference on Formal Methods for Open Object-Based Distributed Systems. 319\u2013333."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303972"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622858","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622858","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622858"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":35,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622858"],"URL":"https:\/\/doi.org\/10.1145\/3622858","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}