C. Luo
A Heap Model for Java Bytecode to Support Separation Logic
Luo, C.; He, G.; Qin, S.
Authors
G. He
S. Qin
Abstract
Memory usage analysis is an important problem for resource-constrained mobile devices, especially under mission- or safety-critical circumstances. Program codes running on or being downloaded into such devices are often available in low-level bytecode forms. We propose in this paper a formal heap model for Java bytecode language, on top of which we can then provide separation logic support for further memory usage verification. Our low-level heap model for Java bytecode would allow us to reason about the size and alignment properties of primitive values stored in the heap. To support type-related reasoning such as guaranteeing type and alignment safety, this model is also lifted with both base types and user-defined classes. Based on such model, we have also defined a separation logic proof system whose assertions are interpreted using the lifted heap with types. We envision, with further extension, the system would provide good support for memory usage analysis and verification for mobile devices.
Citation
Luo, C., He, G., & Qin, S. (2008). A Heap Model for Java Bytecode to Support Separation Logic. In 15th Asia-Pacific Software Engineering Conference, 2-5 December 2008, Beijing, China ; proceedings (127-134). https://doi.org/10.1109/apsec.2008.72
Conference Name | 15th Asia-Pacific Software Engineering Conference (APSEC 2008) |
---|---|
Conference Location | Beijing, China |
Start Date | Dec 3, 2008 |
End Date | Dec 5, 2008 |
Publication Date | Dec 1, 2008 |
Deposit Date | Nov 23, 2009 |
Publicly Available Date | Mar 28, 2024 |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 127-134 |
Book Title | 15th Asia-Pacific Software Engineering Conference, 2-5 December 2008, Beijing, China ; proceedings. |
ISBN | 07695344655 |
DOI | https://doi.org/10.1109/apsec.2008.72 |
Files
Published Conference Proceeding
(155 Kb)
PDF
Copyright Statement
© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
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
Verifying BPEL-like Programs with Hoare Logic
(2008)
Journal Article
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search