UC Riverside

Resource leaks in software systems can result in resource starvation, performance slowdowns, and system crashes. Current techniques aimed at preventing resource leaks face various challenges, including issues of unsoundness, imprecision, inapplicability to existing code, and slow performance.

To address this challenge, our key idea is to simplify leak detection into an accumulation problem—a category of typestate problems amenable to sound and modular checking without the necessity of a heavyweight, whole-program alias analysis. This innovative approach ensures both sound and modular checking, eliminating the requirement for resource-intensive whole-program alias analysis. Despite maintaining soundness, our technique initially demonstrated considerable imprecision. To refine precision, we introduced a specification language to compute targeted aliasing information, a lightweight ownership transfer system, and a mechanism for generating fresh obligations.

Our Java implementation, the Resource Leak Checker, successfully identified 49 real resource leaks in widely-deployed software. The tool demonstrates efficient scaling and

v a manageable false positive rate comparable to the high-confidence resource leak analysis embedded in the Eclipse IDE. However, the precision of our analysis relies on resource management specifications that developers must manually add to the source code, presenting a barrier to practical adoption.

In response, we proposed an inference algorithm designed to capture real-world coding patterns related to resource management. Employing a fixed-point-based approach, the algorithm has been implemented for both Java and C# programming languages. Experimental evaluation illustrates its capability to infer 85.5% of manually written specifications for benchmarks, achieving a true positive rate similar to that obtained with manually added specifications when running the designed resource leak verifiers.

This dissertation outlines a comprehensive solution to prevent resource leaks in software systems. The Resource Leak Checker offers a sound and efficient resource leak detection, while the automated inference algorithm expands the practicality of our specifyand-check verification technique. Experimental results underscore the effectiveness of this approach in ensuring resource leak-free software systems.