Abstract
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 eventually 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 analyzing resource usage as a resource usage analysis
problem, and propose a type-based method as a solution to the problem.