We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Memory usage verification for OO programs.

Chin, W.-N. and Nguyen, H. H. and Qin, S. and Rinard, M. C. (2005) 'Memory usage verification for OO programs.', in Static analysis : 12th International Symposium, SAS 2005, 7-9 September 2005, London, UK ; proceedings. Berlin: Springer, pp. 70-86. Lecture notes in computer science. (3672).


We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that operate on these data structures. Key components of this type system include type assertions that use symbolic Presburger arithmetic expressions to capture data structure sizes, the effect of methods on the data structures that they manipulate, and the amount of memory that methods allocate and deallocate. For each method, we conservatively capture the amount of memory required to execute the method as a function of the sizes of the method’s inputs. The safety guarantee is that the method will never attempt to use more memory than its type expressions specify. We have implemented a type checker to verify memory usages of OO programs. Our experience is that the type system can precisely and effectively capture memory bounds for a wide range of programs.

Item Type:Book chapter
Full text:PDF (Copyright agreement prohibits open access to the full-text) - Accepted Version
Publisher-imposed embargo
Publisher Web site:
Record Created:17 Nov 2009 12:50
Last Modified:09 Oct 2014 10:17

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Usage statisticsLook up in GoogleScholar | Find in a UK Library