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

    123 Downloads (Pure)


    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
    ISBN (Print)9783642169007
    Publication statusPublished - 17 Nov 2010

    Publication series

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


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

    Cite this