Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-04761-9_14
Title: Memory usage verification using Hip/Sleek
Authors: He, G.
Qin, S.
Luo, C.
Chin, W.-N. 
Issue Date: 2009
Source: He, G.,Qin, S.,Luo, C.,Chin, W.-N. (2009). Memory usage verification using Hip/Sleek. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5799 LNCS : 166-181. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-04761-9_14
Abstract: Embedded systems often come with constrained memory footprints. It is therefore essential to ensure that software running on such platforms fulfils memory usage specifications at compile-time, to prevent memory-related software failure after deployment. Previous proposals on memory usage verification are not satisfactory as they usually can only handle restricted subsets of programs, especially when shared mutable data structures are involved. In this paper, we propose a simple but novel solution. We instrument programs with explicit memory operations so that memory usage verification can be done along with the verification of other properties, using an automated verification system Hip/Sleek developed recently by Chin et al.[10,19]. The instrumentation can be done automatically and is proven sound with respect to an underlying semantics. One immediate benefit is that we do not need to develop from scratch a specific system for memory usage verification. Another benefit is that we can verify more programs, especially those involving shared mutable data structures, which previous systems failed to handle, as evidenced by our experimental results. © 2009 Springer-Verlag Berlin Heidelberg.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/42070
ISBN: 3642047602
ISSN: 03029743
DOI: 10.1007/978-3-642-04761-9_14
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

4
checked on Dec 11, 2017

Page view(s)

72
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.