Verifying Heap-Manipulating Programs with Unknown Procedure Calls

Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-ngan Chin

    Research output: Chapter in Book/Report/Conference proceedingChapter

    125 Downloads (Pure)

    Abstract

    Verication of programs with invocations to unknown pro-
    cedures is a practical problem, because in many scenarios not all codes
    of programs to be veried are available. Those unknown calls also pose
    a challenge for their verication. This paper addresses this problem with
    an attempt to verify the full functional correctness of such programs
    using pointer-based data structures. Provided with a Hoare-style speci-
    cation fprg prog fpog where program prog contains calls to some un-
    known procedure unknown, we infer a specication mspecu for unknown
    from the calling contexts, such that the problem of verifying prog can
    be safely reduced to the problem of proving that the procedure unknown
    (once its code is available) meets the derived specication mspecu. The
    expected specication mspecu for the unknown procedure unknown is au-
    tomatically calculated using an abduction-based shape analysis speci-
    cally designed for a combined abstract domain. We have also done some
    experiments to validate the viability of our approach.
    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering
    PublisherSpringer Verlag
    Pages171-187
    ISBN (Print)9783642169007
    DOIs
    Publication statusPublished - 17 Nov 2010

    Publication series

    NameFormal Methods and Software Engineering
    Volume6447
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Fingerprint Dive into the research topics of 'Verifying Heap-Manipulating Programs with Unknown Procedure Calls'. Together they form a unique fingerprint.

  • Cite this

    Qin, S., Luo, C., He, G., Craciun, F., & Chin, W. (2010). Verifying Heap-Manipulating Programs with Unknown Procedure Calls. In Formal Methods and Software Engineering (pp. 171-187). [Chapter 13] (Formal Methods and Software Engineering; Vol. 6447). Springer Verlag. https://doi.org/10.1007/978-3-642-16901-4_13