Memory Usage Verification Using Hip/Sleek

Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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.
    Original languageEnglish
    Title of host publicationAutomated Technology for Verification and Analysis. ATVA 2009
    EditorsZ. Liu, A. P. Ravn
    PublisherSpringer Berlin
    Pages166-181
    Volume5799
    ISBN (Electronic)9783642047619
    ISBN (Print)9783642047602
    DOIs
    Publication statusPublished - 2009
    EventAutomated Technology for Verification and Analysis, 7th International Symposium - Macao, China
    Duration: 14 Oct 200916 Oct 2009
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer, Berlin
    Volume5799

    Conference

    ConferenceAutomated Technology for Verification and Analysis, 7th International Symposium
    Abbreviated titleATVA 2009
    CountryChina
    CityMacao
    Period14/10/0916/10/09

    Fingerprint Dive into the research topics of 'Memory Usage Verification Using Hip/Sleek'. Together they form a unique fingerprint.

  • Cite this

    He, G., Qin, S., Luo, C., & Chin, W-N. (2009). Memory Usage Verification Using Hip/Sleek. In Z. Liu, & A. P. Ravn (Eds.), Automated Technology for Verification and Analysis. ATVA 2009 (Vol. 5799, pp. 166-181). (Lecture Notes in Computer Science; Vol. 5799). Springer Berlin. https://doi.org/10.1007/978-3-642-04761-9_14