Abstract

Various resources such as files and memory are associated with certain protocols about how they should be accessed. For example, a memory cell that has been allocated should be eventually deallocated, and after the deallocation, the cell should no longer be accessed. Igarashi and Kobayashi recently proposed a general type-based method to check whether a program follows such resource access policies, but their analysis was not precise enough for certain programs. In this paper, we refine their type-based analysis by introducing a new notion of time regions. The resulting analysis combines the merits of two major previous approaches to type-based analysis of resource usage -- linear-type-based and effect-based approaches.