Verifying pointer safety for programs with unknown calls

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

    Research output: Contribution to journalArticle

    Abstract

    We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specification in separation logic, where the program contains calls to some unknown procedure , we infer a specification for the unknown procedure from the calling contexts. We show that the problem of verifying the program against the specification can be safely reduced to the problem of proving that the procedure (once its code is available) meets the derived specification . The expected specification for the unknown procedure is automatically calculated using an abduction-based shape analysis. We have also implemented a prototype system to validate the viability of our approach. Preliminary results show that the specifications derived by our tool fully capture the behaviors of the unknown code in many cases.
    Original languageEnglish
    Pages (from-to)1163-1183
    JournalJournal of Symbolic Computation
    Volume45
    Issue number11
    DOIs
    Publication statusPublished - Nov 2010

    Fingerprint Dive into the research topics of 'Verifying pointer safety for programs with unknown calls'. Together they form a unique fingerprint.

  • Cite this