A resource leak occurs when a program allocates a resource, such as a socket or file handle, but fails to deallocate it. Resource leaks can cause severe issues at runtime, motivating static techniques to detect them. Previous techniques for resource leak detection have various drawbacks, such as unsoundness, imprecision, low scalability, or restrictiveness.

In this talk, we first present a new approach to modular and lightweight resource leak verification. Our key insight is that leak detection can be performed soundly without whole-program alias analysis, enabling a modular approach. Precision is achieved with targeted alias tracking, guided by annotations capturing lightweight ownership and resource aliases. Our checker scaled well and revealed 49 real resource leaks in widely-deployed software.

Next, we present a novel inference technique for the annotations required by the resource leak checker. Crucially, our inference technique is designed to infer specifications intended by the developer, even when the code does not fully adhere to that specification. Our technique inferred 85.5% of the annotations that programmers had written manually for our benchmarks, and inferred annotations led to nearly the same false positive rate for the checker as manual annotations.

I’m a Professor at the University of California, Riverside. Previously I worked at IBM Research, Samsung Research, and Uber. My research focuses on developing tools and techniques to make large-scale software more reliable, performant, secure, and maintainable. For more details, see my homepage.