Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.


Durham Research Online
You are in:

Memory usage verification using Hip/Sleek.

He, G. and Qin, S. and Luo, C. and Chin , W.-N. (2009) 'Memory usage verification using Hip/Sleek.', in Automated technology for verification and analysis : 7th International Symposium, ATVA 2009, 14-16 October, 2009, Macao, China ; proceedings. Berlin: Springer, pp. 166-181. Lecture notes in computer science. (5799).

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.

Item Type:Book chapter
Full text:PDF (Copyright agreement prohibits open access to the full-text) - Accepted Version
Publisher-imposed embargo
(256Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/978-3-642-04761-9_14
Record Created:23 Nov 2009 10:35
Last Modified:09 Oct 2014 10:40

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Usage statisticsLook up in GoogleScholar | Find in a UK Library