Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/APSEC.2008.72 | APSEC |
Keywords | Field | DocType |
legal call sequence,temporal specification,api library,heap model,java bytecode,storage management,type-related reasoning,resource-constrained mobile devices,reasoning about programs,verification tool,theorem proving,memory usage analysis,memory usage verification,mobile computing,java,support separation logic,separation logic proof system,formal verification,data models,mobile device,separation logic,cognition | Separation logic,Programming language,Computer science,Heap overflow,Heap (data structure),Binary heap,Java bytecode,Java,Bytecode,Binomial heap | Conference |
ISSN | ISBN | Citations |
1530-1362 | 978-0-7695-3446-6 | 2 |
PageRank | References | Authors |
0.38 | 8 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chenguang Luo | 1 | 56 | 5.63 |
| Guanhua He | 2 | 68 | 7.50 |
| Shengchao Qin | 3 | 711 | 62.81 |