W.N. Chin
Memory Usage Verification for OO Programs
Chin, W.N.; Nguyen, H.H.; Qin, S.; Rinard, M.C.
Authors
H.H. Nguyen
S. Qin
M.C. Rinard
Abstract
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.
Citation
Chin, W., Nguyen, H., Qin, S., & Rinard, M. (2005). Memory Usage Verification for OO Programs. In Static analysis : 12th International Symposium, SAS 2005, 7-9 September 2005, London, UK ; proceedings (70-86). https://doi.org/10.1007/11547662_7
Conference Name | 12th International Static Analysis Symposium (SAS 2005) |
---|---|
Conference Location | London, UK |
Start Date | Sep 7, 2005 |
End Date | Sep 9, 2005 |
Publication Date | Sep 1, 2005 |
Deposit Date | Nov 17, 2009 |
Publicly Available Date | Dec 10, 2009 |
Pages | 70-86 |
Series Title | Lecture notes in computer science |
Series Number | 3672 |
Series ISSN | 0302-9743,1611-3349 |
Book Title | Static analysis : 12th International Symposium, SAS 2005, 7-9 September 2005, London, UK ; proceedings. |
ISBN | 9783540285847 |
DOI | https://doi.org/10.1007/11547662_7 |
Files
Accepted Conference Proceeding
(153 Kb)
PDF
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/11547662_7
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding