Memory Usage Verification for OO Programs

Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

89 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationStatic analysis
Publication statusPublished - 2005
Event12th International Symposium on Static Analysis - London, United Kingdom
Duration: 7 Sep 20059 Sep 2005
Conference number: 12

Publication series

NameStatic Analysis
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Symposium on Static Analysis
Abbreviated titleSAS 2005
Country/TerritoryUnited Kingdom

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).


Dive into the research topics of 'Memory Usage Verification for OO Programs'. Together they form a unique fingerprint.

Cite this