Resource usage analysis

It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should be even-tually deallocated, and after the deallocation, the region should no longer be accessed. A file that has been opened should be eventually closed. So far, most of the methods to analyze this kind of property have been proposed in rather specific contexts (like studies of memory management and verification of usage of lock primitives), and it was not so clear what is the essence of those methods or how methods proposed for individual problems are related. To remedy this situation, we formalize a general problem of analyz-ing resource usage as a resource usage analysis problem, and propose a type-based method as a solution to the problem. 1